From d4e78deb283934c95e37a5775b11363865880794 Mon Sep 17 00:00:00 2001 From: Kenji Maillard Date: Thu, 30 Nov 2023 11:31:11 +0100 Subject: [PATCH] step --- theories/DirectedSemantics.v | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/theories/DirectedSemantics.v b/theories/DirectedSemantics.v index 58d0d33..4bd0714 100644 --- a/theories/DirectedSemantics.v +++ b/theories/DirectedSemantics.v @@ -82,11 +82,18 @@ Section DirectedValid. 1-3: admit. - (* wfTypeProd *) intros Θ A dA B dB d wfA IHA wfB IHB maxd σ τ ϕ rel. - cbn -[subst_term]. - have IHA_ := IHA σ τ ϕ _. + cbn -[subst_term] in *. + have IHA_ := IHA σ τ ϕ rel. remember (compute_dir_and_action (dirs Θ) A σ τ ϕ) as dir_act_A. destruct dir_act_A as [[] actA]; cycle 2. - + have IHB_ := IHB (tRel 0 .: σ) (tRel 0 .: τ) (cons err_term ϕ) _. + + + unshelve epose (IHB_ := IHB (tRel 0 .: σ) (tRel 0 .: τ) (cons err_term ϕ) _). + 1:{ + cbn; split. + 1:tea. + unfold dispatchDir; destruct dA. + all: admit. + } remember (compute_dir_and_action _ B _ _ _) as dir_act_B. destruct dir_act_B as [[] actB]; cycle 2. { split. 1: now constructor. @@ -112,6 +119,7 @@ Section DirectedValid. (* * now trivial. *) (* * admit. *) - (* wfTypeUniv *) + cbn; intros. admit. (* intros Θ d A wtA IHA wfA σ τ l rel. *) (* pose (X := IHA wtA _ _ l rel). *)