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

fix

parent f03c7426
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
theories/typing/type.v
+ 2
− 2
View file @ 249061ad
......@@ -297,7 +297,7 @@ Section type_dist2.
Proof.
intros EQ. eapply dist_later_fin_iff.
destruct n; first done. simpl.
split; intros; try apply EQ; eauto.
split; intros; try apply EQ; eauto with stepindex.
apply dist_S, EQ.
Qed.
Lemma type_later_dist2_later n ty1 ty2 : dist_later n ty1 ty2 → type_dist2_later n ty1 ty2.
......@@ -311,7 +311,7 @@ Section type_dist2.
Proof. intros ?? EQ. apply EQ. Qed.
Lemma ty_own_type_dist n:
Proper (type_dist2 (S n) ==> eq ==> eq ==> dist n) ty_own.
Proof. intros ?? EQ ??-> ??->. apply EQ. eauto. Qed.
Proof. intros ?? EQ ??-> ??->. apply EQ. eauto with stepindex. Qed.
Lemma ty_shr_type_dist n :
Proper (type_dist2 n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
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