1 (*********************************************************************************************************************************)
2 (* HaskProofToStrong: convert HaskProof to HaskStrong *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import NaturalDeduction.
9 Require Import Coq.Strings.String.
10 Require Import Coq.Lists.List.
11 Require Import Coq.Init.Specif.
12 Require Import HaskKinds.
13 Require Import HaskStrongTypes.
14 Require Import HaskStrong.
15 Require Import HaskProof.
17 Section HaskProofToStrong.
19 Context {VV:Type} {eqdec_vv:EqDecidable VV} {freshM:FreshMonad VV}.
21 Definition fresh := FMT_fresh freshM.
22 Definition FreshM := FMT freshM.
23 Definition FreshMon := FMT_Monad freshM.
24 Existing Instance FreshMon.
26 Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
28 Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type :=
30 mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars ->
31 FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
34 Definition judg2exprType (j:Judg) : Type :=
36 (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
37 FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
40 Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ.
45 Definition ileaf `(it:ITree X F [t]) : F t.
50 Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
51 update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q.
61 Lemma quark {T} (l1:list T) l2 vf :
62 (In vf (app l1 l2)) <->
63 (In vf l1) \/ (In vf l2).
90 right; apply H0; auto.
91 right; apply H0; auto.
94 Lemma splitter {T} (l1:list T) l2 vf :
95 (In vf (app l1 l2) → False)
96 -> (In vf l1 → False) /\ (In vf l2 → False).
98 split; intros; apply H; rewrite quark.
104 : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
105 (In vf (leaves tl) -> False) ->
106 mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
112 set (eqd_dec vf t) as x in *.
128 Lemma fresh_lemma'' Γ
129 : forall types ξ lev,
130 FreshM { varstypes : _
131 | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
132 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
137 : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
138 FreshM { varstypes : _
139 | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
140 /\ mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
141 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
144 refine (bind vf = fresh (leaves vars) ; return _).
146 destruct vf as [ vf vf_pf ].
150 set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q.
154 destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
170 intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
172 destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
173 refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_ξ ξ lev
174 (leaves vt2)) _ _; return _).
180 clear IHtypes1 IHtypes2.
181 destruct x1 as [vt1 [pf11 pf12]].
182 exists (vt1,,vt2); split; auto.
184 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
185 set (mapOptionTree_extensional _ _ q) as q'.
192 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
193 set (mapOptionTree_extensional _ _ q) as q'.
197 rewrite <- mapOptionTree_compose.
198 rewrite <- mapOptionTree_compose.
199 rewrite <- mapOptionTree_compose in *.
204 rewrite <- mapOptionTree_compose.
210 Lemma fresh_lemma Γ ξ vars Σ Σ' lev
211 : Σ = mapOptionTree ξ vars ->
213 | mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
214 /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
216 set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
217 refine (q >>>= fun q' => return _).
220 destruct q' as [varstypes [pf1 [pf2 pfdist]]].
221 destruct varstypes; try destruct o; try destruct p; simpl in *.
222 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
223 inversion pf2; subst.
225 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
231 Definition urule2expr : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★),
232 ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j.
234 refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} :
235 ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j :=
236 match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with
237 | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
238 | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
239 | RCanL t a => let case_RCanL := tt in _
240 | RCanR t a => let case_RCanR := tt in _
241 | RuCanL t a => let case_RuCanL := tt in _
242 | RuCanR t a => let case_RuCanR := tt in _
243 | RAssoc t a b c => let case_RAssoc := tt in _
244 | RCossa t a b c => let case_RCossa := tt in _
245 | RExch t a b => let case_RExch := tt in _
246 | RWeak t a => let case_RWeak := tt in _
247 | RCont t a => let case_RCont := tt in _
248 end); clear urule2expr; intros.
251 apply ILeaf; simpl; intros.
254 apply (X0 ([],,vars)).
255 simpl; rewrite <- H; auto.
258 apply ILeaf; simpl; intros.
261 apply (X0 (vars,,[])).
262 simpl; rewrite <- H; auto.
264 destruct case_RuCanL.
265 apply ILeaf; simpl; intros.
266 destruct vars; try destruct o; inversion H.
269 apply (X0 vars2); auto.
271 destruct case_RuCanR.
272 apply ILeaf; simpl; intros.
273 destruct vars; try destruct o; inversion H.
276 apply (X0 vars1); auto.
278 destruct case_RAssoc.
279 apply ILeaf; simpl; intros.
282 destruct vars; try destruct o; inversion H.
283 destruct vars1; try destruct o; inversion H.
284 apply (X0 (vars1_1,,(vars1_2,,vars2))).
287 destruct case_RCossa.
288 apply ILeaf; simpl; intros.
291 destruct vars; try destruct o; inversion H.
292 destruct vars2; try destruct o; inversion H.
293 apply (X0 ((vars1,,vars2_1),,vars2_2)).
297 destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
298 destruct o; [ idtac | apply INone ].
299 destruct u; simpl in *.
300 apply ILeaf; simpl; intros.
301 destruct vars; try destruct o; inversion H.
302 set (fun q => ileaf (e ξ q)) as r'.
304 apply r' with (vars:=vars2).
316 apply X with (vars:=vars1,,vars).
323 apply IHh0_1. inversion X; auto.
324 apply IHh0_2. inversion X; auto.
327 destruct case_RRight.
328 destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
329 destruct o; [ idtac | apply INone ].
330 destruct u; simpl in *.
331 apply ILeaf; simpl; intros.
332 destruct vars; try destruct o; inversion H.
333 set (fun q => ileaf (e ξ q)) as r'.
335 apply r' with (vars:=vars1).
347 apply X with (vars:=vars,,vars2).
354 apply IHh0_1. inversion X; auto.
355 apply IHh0_2. inversion X; auto.
359 apply ILeaf; simpl; intros.
362 destruct vars; try destruct o; inversion H.
363 apply (X0 (vars2,,vars1)).
364 inversion H; subst; auto.
367 apply ILeaf; simpl; intros.
374 apply ILeaf; simpl; intros.
377 apply (X0 (vars,,vars)).
383 Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ :
384 ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c.
388 destruct u; simpl in *.
392 intros; apply it with (vars:=vars); auto.
394 apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto.
397 Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
398 ITree (LeveledHaskType Γ ★)
399 (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
400 (mapOptionTree (ξ' ○ (@fst _ _)) varstypes)
401 -> ELetRecBindings Γ Δ ξ' l varstypes.
404 destruct a; simpl in *.
407 apply ileaf in X. simpl in X.
410 destruct (eqd_dec (unlev (ξ' v)) τ).
414 destruct (eqd_dec h0 l).
417 apply (Prelude_error "level mismatch; should never happen").
418 apply (Prelude_error "letrec type mismatch; should never happen").
422 apply IHvarstypes1; inversion X; auto.
423 apply IHvarstypes2; inversion X; auto.
426 Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
427 refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
428 | INone => T_Leaf None
429 | ILeaf x y => T_Leaf (Some _)
430 | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
435 Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
436 : ITree { x:X & F x } (fun x => J (projT1 x)) t
437 -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t).
439 induction it; simpl in *.
443 simpl; apply IBranch; auto.
446 Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
447 refine (fix rec t := match t with
448 | T_Leaf None => T_Leaf None
449 | T_Leaf (Some x) => T_Leaf (Some _)
450 | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
452 destruct x as [x fx].
453 refine (bind fx' = fx ; return _).
459 Definition case_helper tc Γ Δ lev tbranches avars ξ :
460 forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
461 prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
463 { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
464 & Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars (weakCK'' Δ)) (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)).
469 destruct pcb as [sac pcb].
473 destruct s as [vars vars_pf].
475 refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars
476 (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _).
479 rewrite <- mapOptionTree_compose.
481 destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
482 set (mapOptionTree (@fst _ _) localvars) as localvars'.
484 set (list2vec (leaves localvars')) as localvars''.
485 cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
486 rewrite H'' in localvars''.
487 cut (distinct (vec2list localvars'')). intro H'''.
488 set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
490 refine (bind q = (f (scbwv_ξ scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
495 rewrite <- mapOptionTree_compose.
510 Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) :=
512 | T_Leaf None => return []
513 | T_Leaf (Some x) => bind x' = x ; return [x']
514 | T_Branch b1 b2 => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
517 Definition gather_branch_variables
518 Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
519 ProofCaseBranch tc Γ Δ lev tbranches avars sac})
522 mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
523 -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
524 -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
525 { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
531 destruct a; [ idtac | apply INone ].
533 apply ileaf in source.
535 destruct s as [sac pcb].
547 destruct vars; try destruct o; simpl in pf; inversion pf.
552 apply (IHalts1 vars1 H0 X); auto.
553 apply (IHalts2 vars2 H1 X0); auto.
558 Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
562 refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
563 | RURule a b c d e => let case_RURule := tt in _
564 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
565 | RLit Γ Δ l _ => let case_RLit := tt in _
566 | RVar Γ Δ σ p => let case_RVar := tt in _
567 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
568 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
569 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
570 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
571 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
572 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
573 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
574 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
575 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
576 | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
577 | REmptyGroup _ _ => let case_REmptyGroup := tt in _
578 | RBrak Σ a b c n m => let case_RBrak := tt in _
579 | REsc Σ a b c n m => let case_REsc := tt in _
580 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
581 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
582 end); intro X_; try apply ileaf in X_; simpl in X_.
584 destruct case_RURule.
585 destruct d; try destruct o.
586 apply ILeaf; destruct u; simpl; intros.
587 set (@urule2expr a b _ _ e ξ) as q.
588 set (fun z => ileaf (q z)) as q'.
590 apply q' with (vars:=vars).
595 apply no_urules_with_empty_conclusion in e; inversion e; auto.
596 apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.
599 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
604 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
609 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
614 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
618 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
619 destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
623 destruct case_RGlobal.
624 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
631 refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
633 destruct pf as [ vnew [ pf1 pf2 ]].
634 set (update_ξ ξ x ((⟨vnew, tx ⟩) :: nil)) as ξ' in *.
635 refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
645 apply ELam with (ev:=vnew).
652 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
655 apply ileaf in X. simpl in X.
658 destruct case_RBindingGroup.
659 apply ILeaf; simpl; intros.
664 destruct vars; inversion H.
665 destruct o; inversion H3.
666 refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
678 destruct vars. try destruct o; inversion H.
681 set (X1 ξ vars1 H5) as q1.
682 set (X2 ξ vars2 H6) as q2.
683 refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
690 apply (EApp _ _ _ _ _ _ q1' q2').
695 destruct vars; try destruct o; inversion H.
696 refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
698 destruct pf as [ vnew [ pf1 pf2 ]].
699 set (update_ξ ξ p ((⟨vnew, σ₂ ⟩) :: nil)) as ξ' in *.
704 refine (X0 ξ vars2 _ >>>= fun X0' => _).
707 refine (X ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
720 apply ELet with (ev:=vnew)(tv:=σ₂).
724 destruct case_REmptyGroup.
725 apply ILeaf; simpl; intros.
730 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
735 apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
736 rewrite mapOptionTree_compose.
739 apply ileaf in X. simpl in *.
743 destruct case_RAppCo.
744 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
750 destruct case_RAbsCo.
751 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
756 destruct case_RLetRec.
757 apply ILeaf; simpl; intros.
758 refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
759 destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
760 refine (X_ ((update_ξ ξ t (leaves varstypes)))
761 (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
767 inversion X; subst; clear X.
769 apply (@ELetRec _ _ _ _ _ _ _ varstypes).
770 apply (@letrec_helper Γ Δ t varstypes).
771 rewrite <- pf2 in X1.
772 rewrite mapOptionTree_compose.
778 apply ILeaf; simpl; intros.
785 (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
786 * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
787 rename Σ into body_freevars_types.
788 rename vars into all_freevars.
789 rename X0 into body_expr.
790 rename X into alts_exprs.
792 destruct all_freevars; try destruct o; inversion H.
793 rename all_freevars2 into body_freevars.
794 rename all_freevars1 into alts_freevars.
796 set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
797 set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
798 apply fix_indexing in alts_exprs'.
799 simpl in alts_exprs'.
800 apply unindex_tree in alts_exprs'.
801 simpl in alts_exprs'.
802 apply fix2 in alts_exprs'.
803 apply treeM in alts_exprs'.
805 refine ( alts_exprs' >>>= fun Y =>
807 >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
813 Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
815 fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
816 match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
817 | cnd_weak => let case_nil := tt in INone _ _
818 | cnd_rule h c cnd' r => let case_rule := tt in rule2expr _ _ r (closed2expr' _ cnd')
819 | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
820 end)); clear closed2expr'; intros; subst.
823 Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
824 FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
826 induction Σ; intro ξ.
829 set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
830 refine (q >>>= fun q' => return _).
833 destruct q' as [varstypes [pf1 [pf2 distpf]]].
834 exists (mapOptionTree (@fst _ _) varstypes).
835 exists (update_ξ ξ l (leaves varstypes)).
840 refine (bind f1 = IHΣ1 ξ ; _).
842 destruct f1 as [vars1 [ξ1 pf1]].
843 refine (bind f2 = IHΣ2 ξ1 ; _).
845 destruct f2 as [vars2 [ξ2 pf22]].
847 exists (vars1,,vars2).
855 Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
856 {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
857 FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
859 set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
860 apply closed2expr in cnd.
864 refine (bind ξvars = manyFresh _ Σ ξ0; _).
866 destruct ξvars as [vars ξpf].
867 destruct ξpf as [ξ pf].
868 refine (cnd ξ vars _ >>>= fun it => _).
871 refine (return OK _).
876 End HaskProofToStrong.