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 NaturalDeductionContext.
10 Require Import Coq.Strings.String.
11 Require Import Coq.Lists.List.
12 Require Import Coq.Init.Specif.
13 Require Import HaskKinds.
14 Require Import HaskStrongTypes.
15 Require Import HaskStrong.
16 Require Import HaskProof.
18 Section HaskProofToStrong.
20 Context {VV:Type} {eqdec_vv:EqDecidable VV} {freshM:FreshMonad VV}.
22 Definition fresh := FMT_fresh freshM.
23 Definition FreshM := FMT freshM.
24 Definition FreshMon := FMT_Monad freshM.
25 Existing Instance FreshMon.
27 Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
29 Definition judg2exprType (j:Judg) : Type :=
31 (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
32 FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ)
35 Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l.
40 Definition ileaf `(it:ITree X F [t]) : F t.
45 Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
46 update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q.
56 Lemma quark {T} (l1:list T) l2 vf :
57 (In vf (app l1 l2)) <->
58 (In vf l1) \/ (In vf l2).
85 right; apply H0; auto.
86 right; apply H0; auto.
89 Lemma splitter {T} (l1:list T) l2 vf :
90 (In vf (app l1 l2) → False)
91 -> (In vf l1 → False) /\ (In vf l2 → False).
93 split; intros; apply H; rewrite quark.
99 : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
100 (In vf (leaves tl) -> False) ->
101 mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
107 set (eqd_dec vf t) as x in *.
123 Lemma fresh_lemma'' Γ
124 : forall types ξ lev,
125 FreshM { varstypes : _
126 | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
127 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
132 : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
133 FreshM { varstypes : _
134 | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
135 /\ mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
136 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
139 refine (bind vf = fresh (leaves vars) ; return _).
141 destruct vf as [ vf vf_pf ].
145 set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q.
149 destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
165 intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
167 destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
168 refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev
169 (leaves vt2)) _ _; return _).
175 clear IHtypes1 IHtypes2.
176 destruct x1 as [vt1 [pf11 pf12]].
177 exists (vt1,,vt2); split; auto.
179 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
180 set (mapOptionTree_extensional _ _ q) as q'.
187 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
188 set (mapOptionTree_extensional _ _ q) as q'.
192 rewrite <- mapOptionTree_compose.
193 rewrite <- mapOptionTree_compose.
194 rewrite <- mapOptionTree_compose in *.
199 rewrite <- mapOptionTree_compose.
205 Lemma fresh_lemma Γ ξ vars Σ Σ' lev
206 : Σ = mapOptionTree ξ vars ->
208 | mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
209 /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
211 set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
212 refine (q >>>= fun q' => return _).
215 destruct q' as [varstypes [pf1 [pf2 pfdist]]].
216 destruct varstypes; try destruct o; try destruct p; simpl in *.
217 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
218 inversion pf2; subst.
220 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
226 Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type :=
227 forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ).
229 Definition urule2expr : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
230 ujudg2exprType Γ ξ Δ h t l ->
231 ujudg2exprType Γ ξ Δ j t l
234 refine (fix urule2expr h j t l (r:@Arrange _ h j) ξ {struct r} :
235 ujudg2exprType Γ ξ Δ h t l ->
236 ujudg2exprType Γ ξ Δ j t l :=
237 match r as R in Arrange H C return
238 ujudg2exprType Γ ξ Δ H t l ->
239 ujudg2exprType Γ ξ Δ C t l
241 | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
242 | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
243 | RId a => let case_RId := tt in _
244 | RCanL a => let case_RCanL := tt in _
245 | RCanR a => let case_RCanR := tt in _
246 | RuCanL a => let case_RuCanL := tt in _
247 | RuCanR a => let case_RuCanR := tt in _
248 | RAssoc a b c => let case_RAssoc := tt in _
249 | RCossa a b c => let case_RCossa := tt in _
250 | RExch a b => let case_RExch := tt in _
251 | RWeak a => let case_RWeak := tt in _
252 | RCont a => let case_RCont := tt in _
253 | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)
254 end); clear urule2expr; intros.
260 simpl; unfold ujudg2exprType; intros.
262 apply (X ([],,vars)).
263 simpl; rewrite <- H; auto.
266 simpl; unfold ujudg2exprType; intros.
268 apply (X (vars,,[])).
269 simpl; rewrite <- H; auto.
271 destruct case_RuCanL.
272 simpl; unfold ujudg2exprType; intros.
273 destruct vars; try destruct o; inversion H.
275 apply (X vars2); auto.
277 destruct case_RuCanR.
278 simpl; unfold ujudg2exprType; intros.
279 destruct vars; try destruct o; inversion H.
281 apply (X vars1); auto.
283 destruct case_RAssoc.
284 simpl; unfold ujudg2exprType; intros.
286 destruct vars; try destruct o; inversion H.
287 destruct vars1; try destruct o; inversion H.
288 apply (X (vars1_1,,(vars1_2,,vars2))).
291 destruct case_RCossa.
292 simpl; unfold ujudg2exprType; intros.
294 destruct vars; try destruct o; inversion H.
295 destruct vars2; try destruct o; inversion H.
296 apply (X ((vars1,,vars2_1),,vars2_2)).
300 simpl; unfold ujudg2exprType ; intros.
302 destruct vars; try destruct o; inversion H.
303 apply (X (vars2,,vars1)).
304 inversion H; subst; auto.
307 simpl; unfold ujudg2exprType; intros.
313 simpl; unfold ujudg2exprType ; intros.
315 apply (X (vars,,vars)).
321 intro vars; unfold ujudg2exprType; intro H.
322 destruct vars; try destruct o; inversion H.
323 apply (fun q => e ξ q vars2 H2).
327 unfold ujudg2exprType.
329 apply X with (vars:=vars1,,vars).
335 destruct case_RRight.
336 intro vars; unfold ujudg2exprType; intro H.
337 destruct vars; try destruct o; inversion H.
338 apply (fun q => e ξ q vars1 H1).
342 unfold ujudg2exprType.
344 apply X with (vars:=vars,,vars2).
356 Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
358 (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l)
359 (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes)
360 -> ELetRecBindings Γ Δ ξ' l varstypes.
363 destruct a; simpl in *.
366 apply ileaf in X. simpl in X.
369 destruct (eqd_dec (unlev (ξ' v)) τ).
373 destruct (eqd_dec h0 l).
378 apply (Prelude_error "level mismatch; should never happen").
379 apply (Prelude_error "letrec type mismatch; should never happen").
383 apply IHvarstypes1; inversion X; auto.
384 apply IHvarstypes2; inversion X; auto.
387 Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
388 refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
389 | INone => T_Leaf None
390 | ILeaf x y => T_Leaf (Some _)
391 | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
396 Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
397 : ITree { x:X & F x } (fun x => J (projT1 x)) t
398 -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t).
400 induction it; simpl in *.
404 simpl; apply IBranch; auto.
407 Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
408 refine (fix rec t := match t with
409 | T_Leaf None => T_Leaf None
410 | T_Leaf (Some x) => T_Leaf (Some _)
411 | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
413 destruct x as [x fx].
414 refine (bind fx' = fx ; return _).
420 Definition case_helper tc Γ Δ lev tbranches avars ξ :
421 forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
422 prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
424 { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
425 & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
426 (weakT' tbranches) (weakL' lev) }) (projT1 pcb)).
431 destruct pcb as [sac pcb].
435 destruct s as [vars vars_pf].
437 refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars
438 (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _).
441 rewrite <- mapOptionTree_compose.
443 destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
444 set (mapOptionTree (@fst _ _) localvars) as localvars'.
446 set (list2vec (leaves localvars')) as localvars''.
447 cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
448 rewrite H'' in localvars''.
449 cut (distinct (vec2list localvars'')). intro H'''.
450 set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
452 refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
457 rewrite <- mapOptionTree_compose.
472 Definition gather_branch_variables
473 Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
474 ProofCaseBranch tc Γ Δ lev tbranches avars sac})
477 mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
478 -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
479 -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
480 { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
486 destruct a; [ idtac | apply INone ].
488 apply ileaf in source.
490 destruct s as [sac pcb].
502 destruct vars; try destruct o; simpl in pf; inversion pf.
507 apply (IHalts1 vars1 H0 X); auto.
508 apply (IHalts2 vars2 H1 X0); auto.
513 Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
517 refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
518 | RArrange a b c d e l r => let case_RURule := tt in _
519 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
520 | RLit Γ Δ l _ => let case_RLit := tt in _
521 | RVar Γ Δ σ p => let case_RVar := tt in _
522 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
523 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
524 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
525 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
526 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
527 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
528 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
529 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
530 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
531 | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _
532 | RJoin Γ p lri m x q l => let case_RJoin := tt in _
533 | RVoid _ _ l => let case_RVoid := tt in _
534 | RBrak Σ a b c n m => let case_RBrak := tt in _
535 | REsc Σ a b c n m => let case_REsc := tt in _
536 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
537 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
538 end); intro X_; try apply ileaf in X_; simpl in X_.
540 destruct case_RURule.
541 apply ILeaf. simpl. intros.
542 set (@urule2expr a b _ _ e l r0 ξ) as q.
543 unfold ujudg2exprType.
544 unfold ujudg2exprType in q.
545 apply q with (vars:=vars).
547 apply X_ with (vars:=vars0).
552 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
557 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
562 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
567 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
571 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
572 destruct vars; simpl in H; inversion H; destruct o. inversion H1.
573 set (@EVar _ _ _ Δ ξ v) as q.
579 destruct case_RGlobal.
580 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
586 refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
588 destruct pf as [ vnew [ pf1 pf2 ]].
589 set (update_xi ξ x (((vnew, tx )) :: nil)) as ξ' in *.
590 refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
600 apply ELam with (ev:=vnew).
607 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
610 apply ileaf in X. simpl in X.
614 apply ILeaf; simpl; intros.
619 destruct vars; inversion H.
620 destruct o; inversion H3.
621 refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
633 destruct vars. try destruct o; inversion H.
636 set (X1 ξ vars1 H5) as q1.
637 set (X2 ξ vars2 H6) as q2.
638 refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
645 apply (EApp _ _ _ _ _ _ q1' q2').
650 destruct vars; try destruct o; inversion H.
652 refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
655 destruct pf as [ vnew [ pf1 pf2 ]].
656 set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
662 refine (X ξ vars1 _ >>>= fun X0' => _).
667 refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
679 apply ELet with (ev:=vnew)(tv:=σ₁).
683 destruct case_RWhere.
686 destruct vars; try destruct o; inversion H.
687 destruct vars2; try destruct o; inversion H2.
690 assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto.
691 refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)).
694 destruct pf as [ vnew [ pf1 pf2 ]].
695 set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
701 refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _).
710 refine (X0 ξ vars2_1 _ >>>= fun X1' => _).
719 apply ELet with (ev:=vnew)(tv:=σ₁).
724 apply ILeaf; simpl; intros.
729 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
734 apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
735 rewrite mapOptionTree_compose.
738 apply ileaf in X. simpl in *.
742 destruct case_RAppCo.
743 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
749 destruct case_RAbsCo.
750 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
755 destruct case_RLetRec.
756 apply ILeaf; simpl; intros.
757 refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
758 destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
759 refine (X_ ((update_xi ξ t (leaves varstypes)))
760 (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
766 inversion X; subst; clear X.
768 apply (@ELetRec _ _ _ _ _ _ _ varstypes).
770 apply (@letrec_helper Γ Δ t varstypes).
771 rewrite mapOptionTree_compose.
772 rewrite mapOptionTree_compose.
774 replace ((mapOptionTree unlev (y @@@ t))) with y.
776 clear pf1 X0 X1 pfdist pf2 vars varstypes.
777 induction y; try destruct a; auto.
786 apply ILeaf; simpl; intros.
793 (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
794 * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
795 rename Σ into body_freevars_types.
796 rename vars into all_freevars.
797 rename X0 into body_expr.
798 rename X into alts_exprs.
800 destruct all_freevars; try destruct o; inversion H.
801 rename all_freevars2 into body_freevars.
802 rename all_freevars1 into alts_freevars.
804 set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
805 set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
806 apply fix_indexing in alts_exprs'.
807 simpl in alts_exprs'.
808 apply unindex_tree in alts_exprs'.
809 simpl in alts_exprs'.
810 apply fix2 in alts_exprs'.
811 apply treeM in alts_exprs'.
813 refine ( alts_exprs' >>>= fun Y =>
815 >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
821 Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
822 match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
823 | scnd_weak _ => let case_nil := tt in fun _ => INone _ _
824 | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
825 | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
828 Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
829 FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
831 induction Σ; intro ξ.
834 set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
835 refine (q >>>= fun q' => return _).
838 destruct q' as [varstypes [pf1 [pf2 distpf]]].
839 exists (mapOptionTree (@fst _ _) varstypes).
840 exists (update_xi ξ l (leaves varstypes)).
845 refine (bind f1 = IHΣ1 ξ ; _).
847 destruct f1 as [vars1 [ξ1 pf1]].
848 refine (bind f2 = IHΣ2 ξ1 ; _).
850 destruct f2 as [vars2 [ξ2 pf22]].
852 exists (vars1,,vars2).
860 Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
861 {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
862 FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
864 set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
865 apply closed2expr in cnd.
869 refine (bind ξvars = manyFresh _ Σ ξ0; _).
871 destruct ξvars as [vars ξpf].
872 destruct ξpf as [ξ pf].
873 refine (cnd ξ vars _ >>>= fun it => _).
876 refine (return OK _).
884 End HaskProofToStrong.