more proofs

Beluga-lang · Sep 30, 2024 · 11175da · 11175da
1 parent 2255a00
commit 11175da
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
@@ -983,6 +983,11 @@ Proof with mautosolve 4.
     (* + admit. *)
     (* + admit. *)
     (* + admit. *)
+    assert {{ ⊢ Γ, B ≈ Γ, B' }} by mauto 3.
+    assert {{ Γ , B ⊢ B'[Wk] : Type@i }} by mauto 4.
+    assert {{ Γ, B ⊢ B[Wk] ≈ B'[Wk] : Type@i }} by mauto 3.
+    assert {{ Γ, B' ⊢ B[Wk] ≈ B'[Wk] : Type@i }} by mauto 3.
+    assert {{ ⊢ Γ, B, B[Wk] ≈ Γ, B', B'[Wk] }} by mauto 4.
 
   - eexists.
     eapply exp_sub_typ; mauto 2.