Skip to content
Snippets Groups Projects
Commit b6913305 authored by Simon Spies's avatar Simon Spies
Browse files

fix

parent 0a9f7fc1
Branches
No related tags found
No related merge requests found
This commit is part of merge request !28. Comments created here will be created in the context of that merge request.
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
theories/typing/type.v
+ 2
− 2
View file @ b6913305
...@@ -296,7 +296,7 @@ Section type_dist2. ...@@ -296,7 +296,7 @@ Section type_dist2.
Lemma type_dist2_dist_later n ty1 ty2 : type_dist2 n ty1 ty2 → dist_later n ty1 ty2. Lemma type_dist2_dist_later n ty1 ty2 : type_dist2 n ty1 ty2 → dist_later n ty1 ty2.
Proof. Proof.
intros EQ. eapply dist_later_fin_iff. destruct n; first done. intros EQ. eapply dist_later_fin_iff. destruct n; first done.
split; intros; try apply EQ; try stepindex_solver. split; intros; try apply EQ; try si_solver.
apply dist_S, EQ. apply dist_S, EQ.
Qed. Qed.
Lemma type_later_dist2_later n ty1 ty2 : dist_later n ty1 ty2 → type_dist2_later n ty1 ty2. Lemma type_later_dist2_later n ty1 ty2 : dist_later n ty1 ty2 → type_dist2_later n ty1 ty2.
...@@ -310,7 +310,7 @@ Section type_dist2. ...@@ -310,7 +310,7 @@ Section type_dist2.
Proof. intros ?? EQ. apply EQ. Qed. Proof. intros ?? EQ. apply EQ. Qed.
Lemma ty_own_type_dist n: Lemma ty_own_type_dist n:
Proper (type_dist2 (S n) ==> eq ==> eq ==> dist n) ty_own. Proper (type_dist2 (S n) ==> eq ==> eq ==> dist n) ty_own.
Proof. intros ?? EQ ??-> ??->. apply EQ. stepindex_solver. Qed. Proof. intros ?? EQ ??-> ??->. apply EQ. si_solver. Qed.
Lemma ty_shr_type_dist n : Lemma ty_shr_type_dist n :
Proper (type_dist2 n ==> eq ==> eq ==> eq ==> dist n) ty_shr. Proper (type_dist2 n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed. Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment