From 9768082b0c9842d7906700729308296cf1fd6783 Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita <y.skm24t@gmail.com>
Date: Thu, 7 Apr 2022 16:42:41 +0900
Subject: [PATCH] Minor proof tweak in cell.v
---
theories/typing/lib/cell.v | 15 ++++++---------
1 file changed, 6 insertions(+), 9 deletions(-)
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 6f72f4fe..a4665d1f 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -145,9 +145,8 @@ Section cell.
typed_val cell_new (fn(∅; ty) → cell ty) (λ post '-[a], Φ a ∧ post Φ).
Proof.
eapply type_fn; [apply _|]=> _ ??[?[]]. simpl_subst. via_tr_impl.
- { iApply type_jump; [solve_typing| |].
- { eapply tctx_extract_ctx_elt; [apply tctx_cell_new|solve_typing]. }
- solve_typing. }
+ { iApply type_jump; [solve_typing| |solve_typing].
+ eapply tctx_extract_ctx_elt; [apply tctx_cell_new|solve_typing]. }
by move=> ?[?[]]?/=.
Qed.
@@ -175,9 +174,8 @@ Section cell.
(λ post '-[Φ], ∀a: 𝔄, Φ a → post a).
Proof.
eapply type_fn; [apply _|]=> _ ??[?[]]. simpl_subst. via_tr_impl.
- { iApply type_jump; [solve_typing| |].
- { eapply tctx_extract_ctx_elt; [apply tctx_cell_into_inner|solve_typing]. }
- solve_typing. }
+ { iApply type_jump; [solve_typing| |solve_typing].
+ eapply tctx_extract_ctx_elt; [apply tctx_cell_into_inner|solve_typing]. }
by move=> ?[?[]]?/=.
Qed.
@@ -206,9 +204,8 @@ Section cell.
(λ post '-[a], Φ a ∧ post Φ).
Proof.
eapply type_fn; [apply _|]=> _ ??[?[]]. simpl_subst. via_tr_impl.
- { iApply type_jump; [solve_typing| |].
- { eapply tctx_extract_ctx_elt; [apply tctx_cell_from_box|solve_typing]. }
- solve_typing. }
+ { iApply type_jump; [solve_typing| |solve_typing].
+ eapply tctx_extract_ctx_elt; [apply tctx_cell_from_box|solve_typing]. }
by move=> ?[?[]]?/=.
Qed.
--
GitLab