rewrite app_comm_cons.
reflexivity.
*)
-admit.
+ admit.
Qed.
Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
| ELR_leaf Γ Δ ξ lev v t e => [t]
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
end.
-(*
-Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
- match elrb with
- | ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ lev v _ _ e => [v]
- | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
- end.
-
-Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * HaskType Γ ★):=
- match elrb with
- | ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ lev v t _ e => [(v, t)]
- | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
- end.
-*)
Lemma stripping_nothing_is_inert
{Γ:TypeEnv}
reflexivity.
Qed.
-(* IDEA: use multi-conclusion proofs instead *)
+(* TODO: use multi-conclusion proofs instead *)
Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
| lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
| lrsp_leaf : forall v t e ,
destruct case_ELet; intros; simpl in *.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
- apply nd_prod; [ idtac | apply pf_let].
- clear pf_let.
- eapply nd_comp; [ apply pf_body | idtac ].
- clear pf_body.
+ apply nd_prod.
+ apply pf_let.
+ clear pf_let.
+ eapply nd_comp; [ apply pf_body | idtac ].
+ clear pf_body.
fold (@mapOptionTree VV).
fold (mapOptionTree ξ).
set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.