-Lemma cheat1 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
- eLetRecTypes branches =
- mapOptionTree (update_ξ'' ξ tree lev)
- (mapOptionTree (@fst _ _) tree).
- intros.
- induction branches.
- reflexivity.
- simpl.
- unfold update_ξ.
- unfold mapOptionTree; simpl.
-admit.
-admit.
- Qed.
-Lemma cheat2 : forall Γ Δ ξ l tc tbranches atypes e alts',
-mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
-=
-(*
-((mapOptionTreeAndFlatten
-(fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h)))
- (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)).
-*)
-((mapOptionTreeAndFlatten pcb_freevars
- (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)).
-admit.
-Qed.
-Lemma cheat3 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l).
- admit.
- Qed.
-Lemma cheat4 : forall {A}(t:list A), leaves (unleaves t) = t.
-admit.
-Qed.
-
-Lemma letRecSubproofsToND Γ Δ ξ lev tree branches
- : LetRecSubproofs Γ Δ ξ lev tree branches ->
- ND Rule []
- [ Γ > Δ >
- mapOptionTree ξ (eLetRecContext branches)
- |-
- eLetRecTypes branches
- ].
- intro X.
- induction X; intros; simpl in *.
+Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
+ LetRecSubproofs Γ Δ ξ lev tree branches ->
+ ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
+ |- eLetRecTypes branches @@@ lev ].
+ intro X; induction X; intros; simpl in *.