Require Import Preamble.
Require Import General.
Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Section HaskProofToStrong.
- Context
- {VV:Type}
- {eqdec_vv:EqDecidable VV}
- {fresh: forall (l:list VV), { lf:VV & distinct (lf::l) }}.
+ Context {VV:Type} {eqdec_vv:EqDecidable VV} {freshM:FreshMonad VV}.
- Definition Exprs (Γ:TypeEnv)(Δ:CoercionEnv Γ)(ξ:VV -> LeveledHaskType Γ ★)(τ:Tree ??(LeveledHaskType Γ ★)) :=
- ITree _ (fun τ => Expr Γ Δ ξ τ) τ.
+ Definition fresh := FMT_fresh freshM.
+ Definition FreshM := FMT freshM.
+ Definition FreshMon := FMT_Monad freshM.
+ Existing Instance FreshMon.
+
+ Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
Definition judg2exprType (j:Judg) : Type :=
match j with
- (Γ > Δ > Σ |- τ) => { ξ:VV -> LeveledHaskType Γ ★ & Exprs Γ Δ ξ τ }
+ (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
+ FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ)
end.
- (* reminder: need to pass around uniq-supplies *)
- Definition rule2expr
- : forall h j
- (r:Rule h [j]),
- ITree _ judg2exprType h ->
- judg2exprType j.
-
- intros.
- destruct j.
- refine (match r as R in Rule H C return C=[Γ > Δ > t |- t0] -> _ with
- | RURule a b c d e => let case_RURule := tt in _
- | RNote x n z => let case_RNote := tt in _
- | RLit Γ Δ l _ => let case_RLit := tt in _
- | RVar Γ Δ σ p => let case_RVar := tt in _
- | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
- | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
- | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
- | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
- | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
- | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
- | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
- | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
- | RLetRec Γ p lri x y => let case_RLetRec := tt in _
- | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
- | REmptyGroup _ _ => let case_REmptyGroup := tt in _
- | RCase Σ Γ T κlen κ θ ldcd τ => let case_RCase := tt in _
- | RBrak Σ a b c n m => let case_RBrak := tt in _
- | REsc Σ a b c n m => let case_REsc := tt in _
- end (refl_equal _) ); intros.
+ Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l.
+ intros.
+ inversion X; auto.
+ Defined.
- destruct case_RURule.
- destruct d; [ destruct o | idtac ]; inversion H; subst.
- clear H.
- destruct u.
- refine (match e as R in URule H C return C=[a >> b > t1 |- t2] -> _ with
- | RLeft h c ctx r => let case_RLeft := tt in _
- | RRight h c ctx r => let case_RRight := tt in _
- | RCanL t a => let case_RCanL := tt in _
- | RCanR t a => let case_RCanR := tt in _
- | RuCanL t a => let case_RuCanL := tt in _
- | RuCanR t a => let case_RuCanR := tt in _
- | RAssoc t a b c => let case_RAssoc := tt in _
- | RCossa t a b c => let case_RCossa := tt in _
- | RExch t a b => let case_RExch := tt in _
- | RWeak t a => let case_RWeak := tt in _
- | RCont t a => let case_RCont := tt in _
- end (refl_equal _) ); intros.
-
- destruct case_RCanL. admit.
- destruct case_RCanR. admit.
- destruct case_RuCanL. admit.
- destruct case_RuCanR. admit.
- destruct case_RAssoc. admit.
- destruct case_RCossa. admit.
- destruct case_RLeft. admit.
- destruct case_RRight. admit.
- destruct case_RExch. admit.
- destruct case_RWeak. admit.
- destruct case_RCont. admit.
- destruct case_RBrak. admit.
- destruct case_REsc. admit.
- destruct case_RNote. admit.
- destruct case_RLit. admit.
- destruct case_RVar. admit.
- destruct case_RLam. admit.
- destruct case_RCast. admit.
- destruct case_RBindingGroup. admit.
- destruct case_RApp. admit.
- destruct case_RLet. admit.
- destruct case_REmptyGroup. admit.
- destruct case_RAppT. admit.
- destruct case_RAbsT. admit.
- destruct case_RAppCo. admit.
- destruct case_RAbsCo. admit.
- destruct case_RLetRec. admit.
- destruct case_RCase. admit.
- Defined.
-
- Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
- refine ((
- fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
- match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
- | cnd_weak => let case_nil := tt in _
- | cnd_rule h c cnd' r => let case_rule := tt in (fun rest => _) (closed2expr' _ cnd')
- | cnd_branch _ _ c1 c2 => let case_branch := tt in (fun rest1 rest2 => _) (closed2expr' _ c1) (closed2expr' _ c2)
- end)); clear closed2expr'; intros; subst.
-
- destruct case_nil.
- apply INone.
-
- destruct case_rule.
- set (@rule2expr h) as q.
- destruct c.
- destruct o.
- apply ILeaf.
- eapply rule2expr.
- apply r.
- apply rest.
-
- apply no_rules_with_empty_conclusion in r.
- inversion r.
- auto.
+ Definition ileaf `(it:ITree X F [t]) : F t.
+ inversion it.
+ apply X0.
+ Defined.
+
+ Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
+ update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q.
+ intros.
+ induction l1.
+ reflexivity.
+ simpl.
+ destruct a; simpl.
+ rewrite IHl1.
+ reflexivity.
+ Qed.
+
+ Lemma quark {T} (l1:list T) l2 vf :
+ (In vf (app l1 l2)) <->
+ (In vf l1) \/ (In vf l2).
+ induction l1.
+ simpl; auto.
+ split; intro.
+ right; auto.
+ inversion H.
+ inversion H0.
+ auto.
+ split.
+
+ destruct IHl1.
+ simpl in *.
+ intro.
+ destruct H1.
+ left; left; auto.
+ set (H H1) as q.
+ destruct q.
+ left; right; auto.
+ right; auto.
+ simpl.
+
+ destruct IHl1.
+ simpl in *.
+ intro.
+ destruct H1.
+ destruct H1.
+ left; auto.
+ right; apply H0; auto.
+ right; apply H0; auto.
+ Qed.
+
+ Lemma splitter {T} (l1:list T) l2 vf :
+ (In vf (app l1 l2) → False)
+ -> (In vf l1 → False) /\ (In vf l2 → False).
+ intros.
+ split; intros; apply H; rewrite quark.
+ auto.
+ auto.
+ Qed.
+
+ Lemma helper
+ : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
+ (In vf (leaves tl) -> False) ->
+ mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
+ mapOptionTree ξ tl.
+ intros.
+ induction tl;
+ try destruct a;
+ simpl in *.
+ set (eqd_dec vf t) as x in *.
+ destruct x.
+ subst.
+ assert False.
+ apply H.
+ left; auto.
+ inversion H0.
+ auto.
+ auto.
+ apply splitter in H.
+ destruct H.
+ rewrite (IHtl1 H).
+ rewrite (IHtl2 H0).
+ reflexivity.
+ Qed.
+
+ Lemma fresh_lemma'' Γ
+ : forall types ξ lev,
+ FreshM { varstypes : _
+ | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
+ /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
+ admit.
+ Defined.
+
+ Lemma fresh_lemma' Γ
+ : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
+ FreshM { varstypes : _
+ | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
+ /\ mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
+ /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
+ induction types.
+ intros; destruct a.
+ refine (bind vf = fresh (leaves vars) ; return _).
+ apply FreshMon.
+ destruct vf as [ vf vf_pf ].
+ exists [(vf,h)].
+ split; auto.
+ simpl.
+ set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q.
+ rewrite q.
+ symmetry; auto.
+ simpl.
+ destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
+ split; auto.
+ apply distinct_cons.
+ intro.
+ inversion H0.
+ apply distinct_nil.
+ refine (return _).
+ exists []; auto.
+ split.
+ simpl.
+ symmetry; auto.
+ split.
+ simpl.
+ reflexivity.
+ simpl.
+ apply distinct_nil.
+ intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
+ apply FreshMon.
+ destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
+ refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev
+ (leaves vt2)) _ _; return _).
+ apply FreshMon.
+ simpl.
+ rewrite pf21.
+ rewrite pf22.
+ reflexivity.
+ clear IHtypes1 IHtypes2.
+ destruct x1 as [vt1 [pf11 pf12]].
+ exists (vt1,,vt2); split; auto.
+
+ set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
+ set (mapOptionTree_extensional _ _ q) as q'.
+ rewrite q'.
+ clear q' q.
+ inversion pf11.
+ reflexivity.
+
+ simpl.
+ set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
+ set (mapOptionTree_extensional _ _ q) as q'.
+ rewrite q'.
+ rewrite q'.
+ clear q' q.
+ rewrite <- mapOptionTree_compose.
+ rewrite <- mapOptionTree_compose.
+ rewrite <- mapOptionTree_compose in *.
+ split.
+ destruct pf12.
+ rewrite H.
+ inversion pf11.
+ rewrite <- mapOptionTree_compose.
+ reflexivity.
+
+ admit.
+ Defined.
+
+ Lemma fresh_lemma Γ ξ vars Σ Σ' lev
+ : Σ = mapOptionTree ξ vars ->
+ FreshM { vars' : _
+ | mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
+ /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
+ intros.
+ set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
+ refine (q >>>= fun q' => return _).
+ apply FreshMon.
+ clear q.
+ destruct q' as [varstypes [pf1 [pf2 pfdist]]].
+ destruct varstypes; try destruct o; try destruct p; simpl in *.
+ destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
+ inversion pf2; subst.
+ exists v.
+ destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
+ split; auto.
+ inversion pf2.
+ inversion pf2.
+ Defined.
+
+ Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type :=
+ forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ).
+
+ Definition urule2expr : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
+ ujudg2exprType Γ ξ Δ h t l ->
+ ujudg2exprType Γ ξ Δ j t l
+ .
+ intros Γ Δ.
+ refine (fix urule2expr h j t l (r:@Arrange _ h j) ξ {struct r} :
+ ujudg2exprType Γ ξ Δ h t l ->
+ ujudg2exprType Γ ξ Δ j t l :=
+ match r as R in Arrange H C return
+ ujudg2exprType Γ ξ Δ H t l ->
+ ujudg2exprType Γ ξ Δ C t l
+ with
+ | ALeft h c ctx r => let case_ALeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
+ | ARight h c ctx r => let case_ARight := tt in (fun e => _) (urule2expr _ _ _ _ r)
+ | AId a => let case_AId := tt in _
+ | ACanL a => let case_ACanL := tt in _
+ | ACanR a => let case_ACanR := tt in _
+ | AuCanL a => let case_AuCanL := tt in _
+ | AuCanR a => let case_AuCanR := tt in _
+ | AAssoc a b c => let case_AAssoc := tt in _
+ | AuAssoc a b c => let case_AuAssoc := tt in _
+ | AExch a b => let case_AExch := tt in _
+ | AWeak a => let case_AWeak := tt in _
+ | ACont a => let case_ACont := tt in _
+ | AComp a b c f g => let case_AComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)
+ end); clear urule2expr; intros.
+
+ destruct case_AId.
+ apply X.
+
+ destruct case_ACanL.
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
+ apply (X ([],,vars)).
+ simpl; rewrite <- H; auto.
+
+ destruct case_ACanR.
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
+ apply (X (vars,,[])).
+ simpl; rewrite <- H; auto.
+
+ destruct case_AuCanL.
+ simpl; unfold ujudg2exprType; intros.
+ destruct vars; try destruct o; inversion H.
+ simpl in X.
+ apply (X vars2); auto.
+ destruct case_AuCanR.
+ simpl; unfold ujudg2exprType; intros.
+ destruct vars; try destruct o; inversion H.
+ simpl in X.
+ apply (X vars1); auto.
+
+ destruct case_AAssoc.
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
+ destruct vars; try destruct o; inversion H.
+ destruct vars1; try destruct o; inversion H.
+ apply (X (vars1_1,,(vars1_2,,vars2))).
+ subst; auto.
+
+ destruct case_AuAssoc.
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
+ destruct vars; try destruct o; inversion H.
+ destruct vars2; try destruct o; inversion H.
+ apply (X ((vars1,,vars2_1),,vars2_2)).
+ subst; auto.
+
+ destruct case_AExch.
+ simpl; unfold ujudg2exprType ; intros.
+ simpl in X.
+ destruct vars; try destruct o; inversion H.
+ apply (X (vars2,,vars1)).
+ inversion H; subst; auto.
+
+ destruct case_AWeak.
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
+ apply (X []).
+ auto.
+
+ destruct case_ACont.
+ simpl; unfold ujudg2exprType ; intros.
+ simpl in X.
+ apply (X (vars,,vars)).
simpl.
- apply systemfc_all_rules_one_conclusion in r.
- inversion r.
+ rewrite <- H.
+ auto.
- destruct case_branch.
- apply IBranch.
- apply rest1.
- apply rest2.
+ destruct case_ALeft.
+ intro vars; unfold ujudg2exprType; intro H.
+ destruct vars; try destruct o; inversion H.
+ apply (fun q => e ξ q vars2 H2).
+ clear r0 e H2.
+ simpl in X.
+ simpl.
+ unfold ujudg2exprType.
+ intros.
+ apply X with (vars:=vars1,,vars).
+ rewrite H0.
+ rewrite H1.
+ simpl.
+ reflexivity.
+
+ destruct case_ARight.
+ intro vars; unfold ujudg2exprType; intro H.
+ destruct vars; try destruct o; inversion H.
+ apply (fun q => e ξ q vars1 H1).
+ clear r0 e H2.
+ simpl in X.
+ simpl.
+ unfold ujudg2exprType.
+ intros.
+ apply X with (vars:=vars,,vars2).
+ rewrite H0.
+ inversion H.
+ simpl.
+ reflexivity.
+
+ destruct case_AComp.
+ apply e2.
+ apply e1.
+ apply X.
Defined.
- Definition proof2expr Γ Δ τ Σ : ND Rule [] [Γ > Δ > Σ |- [τ]] -> { ξ:VV -> LeveledHaskType Γ ★ & Expr Γ Δ ξ τ }.
- intro pf.
- set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
- apply closed2expr in cnd.
- inversion cnd; subst.
+ Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
+ ITree (HaskType Γ ★)
+ (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l)
+ (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes)
+ -> ELetRecBindings Γ Δ ξ' l varstypes.
+ intros.
+ induction varstypes.
+ destruct a; simpl in *.
+ destruct p.
+ simpl.
+ apply ileaf in X. simpl in X.
+ apply ELR_leaf.
+ rename h into τ.
+ destruct (eqd_dec (unlev (ξ' v)) τ).
+ rewrite <- e.
+ destruct (ξ' v).
+ simpl.
+ destruct (eqd_dec h0 l).
+ rewrite <- e0.
+ simpl in X.
+ subst.
+ apply X.
+ apply (Prelude_error "level mismatch; should never happen").
+ apply (Prelude_error "letrec type mismatch; should never happen").
+
+ apply ELR_nil.
+ apply ELR_branch.
+ apply IHvarstypes1; inversion X; auto.
+ apply IHvarstypes2; inversion X; auto.
+ Defined.
+
+ Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
+ refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
+ | INone => T_Leaf None
+ | ILeaf x y => T_Leaf (Some _)
+ | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
+ end).
+ exists x; auto.
+ Defined.
+
+ Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
+ : ITree { x:X & F x } (fun x => J (projT1 x)) t
+ -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t).
+ intro it.
+ induction it; simpl in *.
+ apply INone.
+ apply ILeaf.
+ apply f.
+ simpl; apply IBranch; auto.
+ Defined.
+
+ Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
+ refine (fix rec t := match t with
+ | T_Leaf None => T_Leaf None
+ | T_Leaf (Some x) => T_Leaf (Some _)
+ | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
+ end).
+ destruct x as [x fx].
+ refine (bind fx' = fx ; return _).
+ apply FreshMon.
+ exists x.
+ apply fx'.
+ Defined.
+
+ Definition case_helper tc Γ Δ lev tbranches avars ξ :
+ forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
+ prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
+ ((fun sac => FreshM
+ { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
+ & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
+ (weakT' tbranches) (weakL' lev) }) (projT1 pcb)).
+ intro pcb.
+ intro X.
simpl in X.
- clear cnd pf.
+ simpl.
+ destruct pcb as [sac pcb].
+ simpl in *.
+
destruct X.
- exists x.
- inversion e.
+ destruct s as [vars vars_pf].
+
+ refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars
+ (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _).
+ apply FreshMon.
+ rewrite vars_pf.
+ rewrite <- mapOptionTree_compose.
+ reflexivity.
+ destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
+ set (mapOptionTree (@fst _ _) localvars) as localvars'.
+
+ set (list2vec (leaves localvars')) as localvars''.
+ cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
+ rewrite H'' in localvars''.
+ cut (distinct (vec2list localvars'')). intro H'''.
+ set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
+
+ refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
+ apply FreshMon.
+ simpl.
+ unfold scbwv_xi.
+ rewrite vars_pf.
+ rewrite <- mapOptionTree_compose.
+ clear localvars_pf1.
+ simpl.
+ rewrite mapleaves'.
+
+ admit.
+
+ exists scb.
+ apply ileaf in q.
+ apply q.
+
+ admit.
+ admit.
+ Defined.
+
+ Definition gather_branch_variables
+ Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
+ ProofCaseBranch tc Γ Δ lev tbranches avars sac})
+ :
+ forall vars,
+ mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
+ -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
+ -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
+ { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
+ alts.
+ induction alts;
+ intro vars;
+ intro pf;
+ intro source.
+ destruct a; [ idtac | apply INone ].
+ simpl in *.
+ apply ileaf in source.
+ apply ILeaf.
+ destruct s as [sac pcb].
+ simpl in *.
+ split.
+ intros.
+ eapply source.
+ apply H.
+ clear source.
+
+ exists vars.
+ auto.
+
+ simpl in pf.
+ destruct vars; try destruct o; simpl in pf; inversion pf.
+ simpl in source.
+ inversion source.
subst.
+ apply IBranch.
+ apply (IHalts1 vars1 H0 X); auto.
+ apply (IHalts2 vars2 H1 X0); auto.
+
+ Defined.
+
+ Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
+ FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
+ intros Γ Σ.
+ induction Σ; intro ξ.
+ destruct a.
+ destruct l as [τ l].
+ set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
+ refine (q >>>= fun q' => return _).
+ apply FreshMon.
+ clear q.
+ destruct q' as [varstypes [pf1 [pf2 distpf]]].
+ exists (mapOptionTree (@fst _ _) varstypes).
+ exists (update_xi ξ l (leaves varstypes)).
+ symmetry; auto.
+ refine (return _).
+ exists [].
+ exists ξ; auto.
+ refine (bind f1 = IHΣ1 ξ ; _).
+ apply FreshMon.
+ destruct f1 as [vars1 [ξ1 pf1]].
+ refine (bind f2 = IHΣ2 ξ1 ; _).
+ apply FreshMon.
+ destruct f2 as [vars2 [ξ2 pf22]].
+ refine (return _).
+ exists (vars1,,vars2).
+ exists ξ2.
+ simpl.
+ rewrite pf22.
+ rewrite pf1.
+ admit. (* freshness assumption *)
+ Defined.
+
+ Definition rlet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p :
+ forall (X_ : ITree Judg judg2exprType
+ ([Γ > Δ > Σ₁ |- [σ₁] @ p],, [Γ > Δ > [σ₁ @@ p],, Σ₂ |- [σ₂] @ p])),
+ ITree Judg judg2exprType [Γ > Δ > Σ₁,, Σ₂ |- [σ₂] @ p].
+ intros.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+
+ refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
+ apply FreshMon.
+
+ destruct pf as [ vnew [ pf1 pf2 ]].
+ set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
+ inversion X_.
+ apply ileaf in X.
+ apply ileaf in X0.
+ simpl in *.
+
+ refine (X ξ vars1 _ >>>= fun X0' => _).
+ apply FreshMon.
+ simpl.
+ auto.
+
+ refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
+ apply FreshMon.
+ simpl.
+ rewrite pf2.
+ rewrite pf1.
+ reflexivity.
+ apply FreshMon.
+
+ apply ILeaf.
+ apply ileaf in X1'.
+ apply ileaf in X0'.
+ simpl in *.
+ apply ELet with (ev:=vnew)(tv:=σ₁).
+ apply X0'.
+ apply X1'.
+ Defined.
+
+ Definition vartree Γ Δ Σ lev ξ :
+ forall vars, Σ @@@ lev = mapOptionTree ξ vars ->
+ ITree (HaskType Γ ★) (fun t : HaskType Γ ★ => Expr Γ Δ ξ t lev) Σ.
+ induction Σ; intros.
+ destruct a.
+ intros; simpl in *.
+ apply ILeaf.
+ destruct vars; try destruct o; inversion H.
+ set (EVar Γ Δ ξ v) as q.
+ rewrite <- H1 in q.
+ apply q.
+ intros.
+ apply INone.
+ intros.
+ destruct vars; try destruct o; inversion H.
+ apply IBranch.
+ eapply IHΣ1.
+ apply H1.
+ eapply IHΣ2.
+ apply H2.
+ Defined.
+
+
+ Definition rdrop Γ Δ Σ₁ Σ₁₂ a lev :
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a,,Σ₁₂ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *.
+ intros.
+ set (X ξ vars H) as q.
+ simpl in q.
+ refine (q >>>= fun q' => return _).
+ apply FreshMon.
+ inversion q'.
+ apply X0.
+ Defined.
+
+ Definition rdrop' Γ Δ Σ₁ Σ₁₂ a lev :
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂,,a @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *.
+ intros.
+ set (X ξ vars H) as q.
+ simpl in q.
+ refine (q >>>= fun q' => return _).
+ apply FreshMon.
+ inversion q'.
+ auto.
+ Defined.
+
+ Definition rdrop'' Γ Δ Σ₁ Σ₁₂ lev :
+ ITree Judg judg2exprType [Γ > Δ > [],,Σ₁ |- Σ₁₂ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *; intros.
+ eapply X with (vars:=[],,vars).
+ rewrite H; reflexivity.
+ Defined.
+
+ Definition rdrop''' Γ Δ a Σ₁ Σ₁₂ lev :
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > a,,Σ₁ |- Σ₁₂ @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ eapply X with (vars:=vars2).
+ auto.
+ Defined.
+
+ Definition rassoc Γ Δ Σ₁ a b c lev :
+ ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ destruct vars2; try destruct o; inversion H2.
+ apply X with (vars:=(vars1,,vars2_1),,vars2_2).
+ subst; reflexivity.
+ Defined.
+
+ Definition rassoc' Γ Δ Σ₁ a b c lev :
+ ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ destruct vars1; try destruct o; inversion H1.
+ apply X with (vars:=vars1_1,,(vars1_2,,vars2)).
+ subst; reflexivity.
+ Defined.
+
+ Definition swapr Γ Δ Σ₁ a b c lev :
+ ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > ((b,,a),,c) |- Σ₁ @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ destruct vars1; try destruct o; inversion H1.
+ apply X with (vars:=(vars1_2,,vars1_1),,vars2).
+ subst; reflexivity.
+ Defined.
+
+ Definition rdup Γ Δ Σ₁ a c lev :
+ ITree Judg judg2exprType [Γ > Δ > ((a,,a),,c) |- Σ₁ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > (a,,c) |- Σ₁ @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ apply X with (vars:=(vars1,,vars1),,vars2). (* is this allowed? *)
+ subst; reflexivity.
+ Defined.
+
+ (* holy cow this is ugly *)
+ Definition rcut Γ Δ Σ₃ lev Σ₁₂ :
+ forall Σ₁ Σ₂,
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > Σ₁₂ @@@ lev,,Σ₂ |- [Σ₃] @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > Σ₁,,Σ₂ |- [Σ₃] @ lev].
+
+ induction Σ₁₂.
+ intros.
+ destruct a.
+
+ eapply rlet.
+ apply IBranch.
apply X.
+ apply X0.
+
+ simpl in X0.
+ apply rdrop'' in X0.
+ apply rdrop'''.
+ apply X0.
+
+ intros.
+ simpl in X0.
+ apply rassoc in X0.
+ set (IHΣ₁₂1 _ _ (rdrop _ _ _ _ _ _ X) X0) as q.
+ set (IHΣ₁₂2 _ (Σ₁,,Σ₂) (rdrop' _ _ _ _ _ _ X)) as q'.
+ apply rassoc' in q.
+ apply swapr in q.
+ apply rassoc in q.
+ set (q' q) as q''.
+ apply rassoc' in q''.
+ apply rdup in q''.
+ apply q''.
+ Defined.
+
+ Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
+
+ intros h j r.
+
+ refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
+ | RArrange a b c d e l r => let case_RURule := tt in _
+ | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
+ | RLit Γ Δ l _ => let case_RLit := tt in _
+ | RVar Γ Δ σ p => let case_RVar := tt in _
+ | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
+ | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
+ | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
+ | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
+ | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
+ | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
+ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
+ | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
+ | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
+ | RCut Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
+ | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
+ | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _
+ | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _
+ | RVoid _ _ l => let case_RVoid := tt in _
+ | RBrak Σ a b c n m => let case_RBrak := tt in _
+ | REsc Σ a b c n m => let case_REsc := tt in _
+ | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
+ | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
+ end); intro X_; try apply ileaf in X_; simpl in X_.
+
+ destruct case_RURule.
+ apply ILeaf. simpl. intros.
+ set (@urule2expr a b _ _ e l r0 ξ) as q.
+ unfold ujudg2exprType.
+ unfold ujudg2exprType in q.
+ apply q with (vars:=vars).
+ intros.
+ apply X_ with (vars:=vars0).
+ auto.
+ auto.
+
+ destruct case_RBrak.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
+ apply EBrak.
+ apply (ileaf X).
+
+ destruct case_REsc.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
+ apply EEsc.
+ apply (ileaf X).
+
+ destruct case_RNote.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
+ apply ENote; auto.
+ apply (ileaf X).
+
+ destruct case_RLit.
+ apply ILeaf; simpl; intros; refine (return ILeaf _ _).
+ apply ELit.
+
+ destruct case_RVar.
+ apply ILeaf; simpl; intros; refine (return ILeaf _ _).
+ destruct vars; simpl in H; inversion H; destruct o. inversion H1.
+ set (@EVar _ _ _ Δ ξ v) as q.
+ rewrite <- H2 in q.
+ simpl in q.
+ apply q.
+ inversion H.
+
+ destruct case_RGlobal.
+ apply ILeaf; simpl; intros; refine (return ILeaf _ _).
+ apply EGlobal.
+
+ destruct case_RLam.
+ apply ILeaf.
+ simpl in *; intros.
+ refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
+ apply FreshMon.
+ destruct pf as [ vnew [ pf1 pf2 ]].
+ set (update_xi ξ x (((vnew, tx )) :: nil)) as ξ' in *.
+ refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
+ apply FreshMon.
+ simpl.
+ rewrite pf1.
+ rewrite <- pf2.
+ simpl.
+ reflexivity.
+ intro hyp.
+ refine (return _).
+ apply ILeaf.
+ apply ELam with (ev:=vnew).
+ apply ileaf in hyp.
+ simpl in hyp.
+ unfold ξ' in hyp.
+ apply hyp.
+
+ destruct case_RCast.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
+ eapply ECast.
+ apply x.
+ apply ileaf in X. simpl in X.
+ apply X.
+
+ destruct case_RApp.
+ apply ILeaf.
+ inversion X_.
+ inversion X.
+ inversion X0.
+ simpl in *.
+ intros.
+ destruct vars. try destruct o; inversion H.
+ simpl in H.
+ inversion H.
+ set (X1 ξ vars1 H5) as q1.
+ set (X2 ξ vars2 H6) as q2.
+ refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
+ apply FreshMon.
+ apply FreshMon.
+ apply ILeaf.
+ apply ileaf in q1'.
+ apply ileaf in q2'.
+ simpl in *.
+ apply (EApp _ _ _ _ _ _ q1' q2').
+
+ destruct case_RLet.
+ eapply rlet.
+ apply X_.
+
+ destruct case_RWhere.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ destruct vars2; try destruct o; inversion H2.
+ clear H2.
+
+ assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto.
+ refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)).
+ apply FreshMon.
+
+ destruct pf as [ vnew [ pf1 pf2 ]].
+ set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
+ inversion X_.
+ apply ileaf in X.
+ apply ileaf in X0.
+ simpl in *.
+
+ refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _).
+ apply FreshMon.
+ simpl.
+ inversion pf1.
+ rewrite H3.
+ rewrite H4.
+ rewrite pf2.
+ reflexivity.
+
+ refine (X0 ξ vars2_1 _ >>>= fun X1' => _).
+ apply FreshMon.
+ reflexivity.
+ apply FreshMon.
+
+ apply ILeaf.
+ apply ileaf in X0'.
+ apply ileaf in X1'.
+ simpl in *.
+ apply ELet with (ev:=vnew)(tv:=σ₁).
+ apply X1'.
+ apply X0'.
+
+ destruct case_RCut.
+ inversion X_.
+ subst.
+ clear X_.
+ induction Σ₃.
+ destruct a.
+ subst.
+ eapply rcut.
+ apply X.
+ apply X0.
+
+ apply ILeaf.
+ simpl.
+ intros.
+ refine (return _).
+ apply INone.
+ set (IHΣ₃1 (rdrop _ _ _ _ _ _ X0)) as q1.
+ set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2.
+ apply ileaf in q1.
+ apply ileaf in q2.
+ simpl in *.
+ apply ILeaf.
+ simpl.
+ intros.
+ refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _).
+ apply FreshMon.
+ apply FreshMon.
+ apply IBranch; auto.
+
+ destruct case_RLeft.
+ apply ILeaf.
+ simpl; intros.
+ destruct vars; try destruct o; inversion H.
+ refine (X_ _ _ H2 >>>= fun X' => return _).
+ apply FreshMon.
+ apply IBranch.
+ eapply vartree.
+ apply H1.
+ apply X'.
+
+ destruct case_RRight.
+ apply ILeaf.
+ simpl; intros.
+ destruct vars; try destruct o; inversion H.
+ refine (X_ _ _ H1 >>>= fun X' => return _).
+ apply FreshMon.
+ apply IBranch.
+ apply X'.
+ eapply vartree.
+ apply H2.
+
+ destruct case_RVoid.
+ apply ILeaf; simpl; intros.
+ refine (return _).
+ apply INone.
+
+ destruct case_RAppT.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
+ apply ETyApp.
+ apply (ileaf X).
+
+ destruct case_RAbsT.
+ apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
+ rewrite mapOptionTree_compose.
+ rewrite <- H.
+ reflexivity.
+ apply ileaf in X. simpl in *.
+ apply ETyLam.
+ apply X.
+
+ destruct case_RAppCo.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
+ auto.
+ eapply ECoApp.
+ apply γ.
+ apply (ileaf X).
+
+ destruct case_RAbsCo.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
+ auto.
+ eapply ECoLam.
+ apply (ileaf X).
+
+ destruct case_RLetRec.
+ apply ILeaf; simpl; intros.
+ refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
+ destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
+ refine (X_ ((update_xi ξ t (leaves varstypes)))
+ (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
+ simpl.
+ rewrite pf2.
+ rewrite pf1.
+ auto.
+ apply ILeaf.
+ inversion X; subst; clear X.
+
+ apply (@ELetRec _ _ _ _ _ _ _ varstypes).
+ auto.
+ apply (@letrec_helper Γ Δ t varstypes).
+ rewrite mapOptionTree_compose.
+ rewrite mapOptionTree_compose.
+ rewrite pf2.
+ replace ((mapOptionTree unlev (y @@@ t))) with y.
+ apply X0.
+ clear pf1 X0 X1 pfdist pf2 vars varstypes.
+ induction y; try destruct a; auto.
+ rewrite IHy1 at 1.
+ rewrite IHy2 at 1.
+ reflexivity.
+ apply ileaf in X1.
+ simpl in X1.
+ apply X1.
+
+ destruct case_RCase.
+ apply ILeaf; simpl; intros.
+ inversion X_.
+ clear X_.
+ subst.
+ apply ileaf in X0.
+ simpl in X0.
+
+ (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
+ * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
+ rename Σ into body_freevars_types.
+ rename vars into all_freevars.
+ rename X0 into body_expr.
+ rename X into alts_exprs.
+
+ destruct all_freevars; try destruct o; inversion H.
+ rename all_freevars2 into body_freevars.
+ rename all_freevars1 into alts_freevars.
+
+ set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
+ set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
+ apply fix_indexing in alts_exprs'.
+ simpl in alts_exprs'.
+ apply unindex_tree in alts_exprs'.
+ simpl in alts_exprs'.
+ apply fix2 in alts_exprs'.
+ apply treeM in alts_exprs'.
+
+ refine ( alts_exprs' >>>= fun Y =>
+ body_expr ξ _ _
+ >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
+ apply FreshMon.
+ apply FreshMon.
+ apply H2.
+ Defined.
+
+ Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
+ match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
+ | scnd_weak _ => let case_nil := tt in fun _ => INone _ _
+ | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
+ | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
+ end.
+
+ Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
+ {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
+ FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
+ intro pf.
+ set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
+ apply closed2expr in cnd.
+ apply ileaf in cnd.
+ simpl in *.
+ clear pf.
+ refine (bind ξvars = manyFresh _ Σ ξ0; _).
+ apply FreshMon.
+ destruct ξvars as [vars ξpf].
+ destruct ξpf as [ξ pf].
+ refine (cnd ξ vars _ >>>= fun it => _).
+ apply FreshMon.
+ auto.
+ refine (return OK _).
+ exists ξ.
+ apply ileaf in it.
+ simpl in it.
+ apply it.
+ apply INone.
Defined.
End HaskProofToStrong.
projects / coq-hetmet.git / blobdiff