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 Definition gather_branch_variables
511 Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
512 ProofCaseBranch tc Γ Δ lev tbranches avars sac})
515 mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
516 -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
517 -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
518 { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
524 destruct a; [ idtac | apply INone ].
526 apply ileaf in source.
528 destruct s as [sac pcb].
540 destruct vars; try destruct o; simpl in pf; inversion pf.
545 apply (IHalts1 vars1 H0 X); auto.
546 apply (IHalts2 vars2 H1 X0); auto.
551 Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
555 refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
556 | RURule a b c d e => let case_RURule := tt in _
557 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
558 | RLit Γ Δ l _ => let case_RLit := tt in _
559 | RVar Γ Δ σ p => let case_RVar := tt in _
560 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
561 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
562 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
563 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
564 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
565 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
566 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
567 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
568 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
569 | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
570 | REmptyGroup _ _ => let case_REmptyGroup := tt in _
571 | RBrak Σ a b c n m => let case_RBrak := tt in _
572 | REsc Σ a b c n m => let case_REsc := tt in _
573 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
574 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
575 end); intro X_; try apply ileaf in X_; simpl in X_.
577 destruct case_RURule.
578 destruct d; try destruct o.
579 apply ILeaf; destruct u; simpl; intros.
580 set (@urule2expr a b _ _ e ξ) as q.
581 set (fun z => ileaf (q z)) as q'.
583 apply q' with (vars:=vars).
588 apply no_urules_with_empty_conclusion in e; inversion e; auto.
589 apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.
592 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
597 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
602 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
607 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
611 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
612 destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
616 destruct case_RGlobal.
617 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
624 refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
626 destruct pf as [ vnew [ pf1 pf2 ]].
627 set (update_ξ ξ x ((⟨vnew, tx ⟩) :: nil)) as ξ' in *.
628 refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
638 apply ELam with (ev:=vnew).
645 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
648 apply ileaf in X. simpl in X.
651 destruct case_RBindingGroup.
652 apply ILeaf; simpl; intros.
657 destruct vars; inversion H.
658 destruct o; inversion H3.
659 refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
671 destruct vars. try destruct o; inversion H.
674 set (X1 ξ vars1 H5) as q1.
675 set (X2 ξ vars2 H6) as q2.
676 refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
683 apply (EApp _ _ _ _ _ _ q1' q2').
688 destruct vars; try destruct o; inversion H.
689 refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
691 destruct pf as [ vnew [ pf1 pf2 ]].
692 set (update_ξ ξ p ((⟨vnew, σ₂ ⟩) :: nil)) as ξ' in *.
697 refine (X0 ξ vars2 _ >>>= fun X0' => _).
700 refine (X ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
713 apply ELet with (ev:=vnew)(tv:=σ₂).
717 destruct case_REmptyGroup.
718 apply ILeaf; simpl; intros.
723 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
728 apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
729 rewrite mapOptionTree_compose.
732 apply ileaf in X. simpl in *.
736 destruct case_RAppCo.
737 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
743 destruct case_RAbsCo.
744 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
749 destruct case_RLetRec.
750 apply ILeaf; simpl; intros.
751 refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
752 destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
753 refine (X_ ((update_ξ ξ t (leaves varstypes)))
754 (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
760 inversion X; subst; clear X.
762 apply (@ELetRec _ _ _ _ _ _ _ varstypes).
763 apply (@letrec_helper Γ Δ t varstypes).
764 rewrite <- pf2 in X1.
765 rewrite mapOptionTree_compose.
771 apply ILeaf; simpl; intros.
778 (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
779 * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
780 rename Σ into body_freevars_types.
781 rename vars into all_freevars.
782 rename X0 into body_expr.
783 rename X into alts_exprs.
785 destruct all_freevars; try destruct o; inversion H.
786 rename all_freevars2 into body_freevars.
787 rename all_freevars1 into alts_freevars.
789 set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
790 set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
791 apply fix_indexing in alts_exprs'.
792 simpl in alts_exprs'.
793 apply unindex_tree in alts_exprs'.
794 simpl in alts_exprs'.
795 apply fix2 in alts_exprs'.
796 apply treeM in alts_exprs'.
798 refine ( alts_exprs' >>>= fun Y =>
800 >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
806 Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
808 fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
809 match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
810 | cnd_weak => let case_nil := tt in INone _ _
811 | cnd_rule h c cnd' r => let case_rule := tt in rule2expr _ _ r (closed2expr' _ cnd')
812 | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
813 end)); clear closed2expr'; intros; subst.
816 Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
817 FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
819 induction Σ; intro ξ.
822 set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
823 refine (q >>>= fun q' => return _).
826 destruct q' as [varstypes [pf1 [pf2 distpf]]].
827 exists (mapOptionTree (@fst _ _) varstypes).
828 exists (update_ξ ξ l (leaves varstypes)).
833 refine (bind f1 = IHΣ1 ξ ; _).
835 destruct f1 as [vars1 [ξ1 pf1]].
836 refine (bind f2 = IHΣ2 ξ1 ; _).
838 destruct f2 as [vars2 [ξ2 pf22]].
840 exists (vars1,,vars2).
848 Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
849 {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
850 FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
852 set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
853 apply closed2expr in cnd.
857 refine (bind ξvars = manyFresh _ Σ ξ0; _).
859 destruct ξvars as [vars ξpf].
860 destruct ξpf as [ξ pf].
861 refine (cnd ξ vars _ >>>= fun it => _).
864 refine (return OK _).
869 End HaskProofToStrong.