Skip to content
Snippets Groups Projects

fix for iris!886 and iris!896

Merged fix for iris!886 and iris!896
msammler/new_contractive into master
All threads resolved!
Merged Michael Sammler requested to merge msammler/new_contractive into master
All threads resolved!
Viewing commit b6913305
Show latest version
1 file
+ 2
− 2
Compare changes
  • Side-by-side
  • Inline
theories/typing/type.v
+ 2
− 2
@@ -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.
Proof.
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.
Qed.
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.
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. stepindex_solver. Qed.
Proof. intros ?? EQ ??-> ??->. apply EQ. si_solver. Qed.
Lemma ty_shr_type_dist n :
Proper (type_dist2 n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.