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 judg2exprType (j:Judg) : Type :=
30 (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
31 FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ)
34 Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l.
39 Definition ileaf `(it:ITree X F [t]) : F t.
44 Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
45 update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q.
55 Lemma quark {T} (l1:list T) l2 vf :
56 (In vf (app l1 l2)) <->
57 (In vf l1) \/ (In vf l2).
84 right; apply H0; auto.
85 right; apply H0; auto.
88 Lemma splitter {T} (l1:list T) l2 vf :
89 (In vf (app l1 l2) → False)
90 -> (In vf l1 → False) /\ (In vf l2 → False).
92 split; intros; apply H; rewrite quark.
98 : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
99 (In vf (leaves tl) -> False) ->
100 mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
106 set (eqd_dec vf t) as x in *.
122 Lemma fresh_lemma'' Γ
123 : forall types ξ lev,
124 FreshM { varstypes : _
125 | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
126 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
131 : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
132 FreshM { varstypes : _
133 | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
134 /\ mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
135 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
138 refine (bind vf = fresh (leaves vars) ; return _).
140 destruct vf as [ vf vf_pf ].
144 set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q.
148 destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
164 intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
166 destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
167 refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev
168 (leaves vt2)) _ _; return _).
174 clear IHtypes1 IHtypes2.
175 destruct x1 as [vt1 [pf11 pf12]].
176 exists (vt1,,vt2); split; auto.
178 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
179 set (mapOptionTree_extensional _ _ q) as q'.
186 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
187 set (mapOptionTree_extensional _ _ q) as q'.
191 rewrite <- mapOptionTree_compose.
192 rewrite <- mapOptionTree_compose.
193 rewrite <- mapOptionTree_compose in *.
198 rewrite <- mapOptionTree_compose.
204 Lemma fresh_lemma Γ ξ vars Σ Σ' lev
205 : Σ = mapOptionTree ξ vars ->
207 | mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
208 /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
210 set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
211 refine (q >>>= fun q' => return _).
214 destruct q' as [varstypes [pf1 [pf2 pfdist]]].
215 destruct varstypes; try destruct o; try destruct p; simpl in *.
216 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
217 inversion pf2; subst.
219 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
225 Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type :=
226 forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ).
228 Definition urule2expr : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
229 ujudg2exprType Γ ξ Δ h t l ->
230 ujudg2exprType Γ ξ Δ j t l
233 refine (fix urule2expr h j t l (r:@Arrange _ h j) ξ {struct r} :
234 ujudg2exprType Γ ξ Δ h t l ->
235 ujudg2exprType Γ ξ Δ j t l :=
236 match r as R in Arrange H C return
237 ujudg2exprType Γ ξ Δ H t l ->
238 ujudg2exprType Γ ξ Δ C t l
240 | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
241 | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
242 | RId a => let case_RId := tt in _
243 | RCanL a => let case_RCanL := tt in _
244 | RCanR a => let case_RCanR := tt in _
245 | RuCanL a => let case_RuCanL := tt in _
246 | RuCanR a => let case_RuCanR := tt in _
247 | RAssoc a b c => let case_RAssoc := tt in _
248 | RCossa a b c => let case_RCossa := tt in _
249 | RExch a b => let case_RExch := tt in _
250 | RWeak a => let case_RWeak := tt in _
251 | RCont a => let case_RCont := tt in _
252 | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)
253 end); clear urule2expr; intros.
259 simpl; unfold ujudg2exprType; intros.
261 apply (X ([],,vars)).
262 simpl; rewrite <- H; auto.
265 simpl; unfold ujudg2exprType; intros.
267 apply (X (vars,,[])).
268 simpl; rewrite <- H; auto.
270 destruct case_RuCanL.
271 simpl; unfold ujudg2exprType; intros.
272 destruct vars; try destruct o; inversion H.
274 apply (X vars2); auto.
276 destruct case_RuCanR.
277 simpl; unfold ujudg2exprType; intros.
278 destruct vars; try destruct o; inversion H.
280 apply (X vars1); auto.
282 destruct case_RAssoc.
283 simpl; unfold ujudg2exprType; intros.
285 destruct vars; try destruct o; inversion H.
286 destruct vars1; try destruct o; inversion H.
287 apply (X (vars1_1,,(vars1_2,,vars2))).
290 destruct case_RCossa.
291 simpl; unfold ujudg2exprType; intros.
293 destruct vars; try destruct o; inversion H.
294 destruct vars2; try destruct o; inversion H.
295 apply (X ((vars1,,vars2_1),,vars2_2)).
299 simpl; unfold ujudg2exprType ; intros.
301 destruct vars; try destruct o; inversion H.
302 apply (X (vars2,,vars1)).
303 inversion H; subst; auto.
306 simpl; unfold ujudg2exprType; intros.
312 simpl; unfold ujudg2exprType ; intros.
314 apply (X (vars,,vars)).
320 intro vars; unfold ujudg2exprType; intro H.
321 destruct vars; try destruct o; inversion H.
322 apply (fun q => e ξ q vars2 H2).
326 unfold ujudg2exprType.
328 apply X with (vars:=vars1,,vars).
334 destruct case_RRight.
335 intro vars; unfold ujudg2exprType; intro H.
336 destruct vars; try destruct o; inversion H.
337 apply (fun q => e ξ q vars1 H1).
341 unfold ujudg2exprType.
343 apply X with (vars:=vars,,vars2).
355 Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
357 (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l)
358 (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes)
359 -> ELetRecBindings Γ Δ ξ' l varstypes.
362 destruct a; simpl in *.
365 apply ileaf in X. simpl in X.
368 destruct (eqd_dec (unlev (ξ' v)) τ).
372 destruct (eqd_dec h0 l).
377 apply (Prelude_error "level mismatch; should never happen").
378 apply (Prelude_error "letrec type mismatch; should never happen").
382 apply IHvarstypes1; inversion X; auto.
383 apply IHvarstypes2; inversion X; auto.
386 Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
387 refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
388 | INone => T_Leaf None
389 | ILeaf x y => T_Leaf (Some _)
390 | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
395 Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
396 : ITree { x:X & F x } (fun x => J (projT1 x)) t
397 -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t).
399 induction it; simpl in *.
403 simpl; apply IBranch; auto.
406 Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
407 refine (fix rec t := match t with
408 | T_Leaf None => T_Leaf None
409 | T_Leaf (Some x) => T_Leaf (Some _)
410 | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
412 destruct x as [x fx].
413 refine (bind fx' = fx ; return _).
419 Definition case_helper tc Γ Δ lev tbranches avars ξ :
420 forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
421 prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
423 { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
424 & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
425 (weakT' tbranches) (weakL' lev) }) (projT1 pcb)).
430 destruct pcb as [sac pcb].
434 destruct s as [vars vars_pf].
436 refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars
437 (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _).
440 rewrite <- mapOptionTree_compose.
442 destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
443 set (mapOptionTree (@fst _ _) localvars) as localvars'.
445 set (list2vec (leaves localvars')) as localvars''.
446 cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
447 rewrite H'' in localvars''.
448 cut (distinct (vec2list localvars'')). intro H'''.
449 set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
451 refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
456 rewrite <- mapOptionTree_compose.
471 Definition gather_branch_variables
472 Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
473 ProofCaseBranch tc Γ Δ lev tbranches avars sac})
476 mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
477 -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
478 -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
479 { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
485 destruct a; [ idtac | apply INone ].
487 apply ileaf in source.
489 destruct s as [sac pcb].
501 destruct vars; try destruct o; simpl in pf; inversion pf.
506 apply (IHalts1 vars1 H0 X); auto.
507 apply (IHalts2 vars2 H1 X0); auto.
512 Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
516 refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
517 | RArrange a b c d e l r => let case_RURule := tt in _
518 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
519 | RLit Γ Δ l _ => let case_RLit := tt in _
520 | RVar Γ Δ σ p => let case_RVar := tt in _
521 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
522 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
523 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
524 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
525 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
526 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
527 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
528 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
529 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
530 | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _
531 | RJoin Γ p lri m x q l => let case_RJoin := tt in _
532 | RVoid _ _ l => let case_RVoid := tt in _
533 | RBrak Σ a b c n m => let case_RBrak := tt in _
534 | REsc Σ a b c n m => let case_REsc := tt in _
535 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
536 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
537 end); intro X_; try apply ileaf in X_; simpl in X_.
539 destruct case_RURule.
540 apply ILeaf. simpl. intros.
541 set (@urule2expr a b _ _ e l r0 ξ) as q.
542 unfold ujudg2exprType.
543 unfold ujudg2exprType in q.
544 apply q with (vars:=vars).
546 apply X_ with (vars:=vars0).
551 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
556 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
561 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
566 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
570 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
571 destruct vars; simpl in H; inversion H; destruct o. inversion H1.
572 set (@EVar _ _ _ Δ ξ v) as q.
578 destruct case_RGlobal.
579 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
585 refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
587 destruct pf as [ vnew [ pf1 pf2 ]].
588 set (update_xi ξ x (((vnew, tx )) :: nil)) as ξ' in *.
589 refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
599 apply ELam with (ev:=vnew).
606 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
609 apply ileaf in X. simpl in X.
613 apply ILeaf; simpl; intros.
618 destruct vars; inversion H.
619 destruct o; inversion H3.
620 refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
632 destruct vars. try destruct o; inversion H.
635 set (X1 ξ vars1 H5) as q1.
636 set (X2 ξ vars2 H6) as q2.
637 refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
644 apply (EApp _ _ _ _ _ _ q1' q2').
649 destruct vars; try destruct o; inversion H.
651 refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
654 destruct pf as [ vnew [ pf1 pf2 ]].
655 set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
661 refine (X ξ vars1 _ >>>= fun X0' => _).
666 refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
678 apply ELet with (ev:=vnew)(tv:=σ₁).
682 destruct case_RWhere.
685 destruct vars; try destruct o; inversion H.
686 destruct vars2; try destruct o; inversion H2.
689 assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto.
690 refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)).
693 destruct pf as [ vnew [ pf1 pf2 ]].
694 set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
700 refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _).
709 refine (X0 ξ vars2_1 _ >>>= fun X1' => _).
718 apply ELet with (ev:=vnew)(tv:=σ₁).
723 apply ILeaf; simpl; intros.
728 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
733 apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
734 rewrite mapOptionTree_compose.
737 apply ileaf in X. simpl in *.
741 destruct case_RAppCo.
742 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
748 destruct case_RAbsCo.
749 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
754 destruct case_RLetRec.
755 apply ILeaf; simpl; intros.
756 refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
757 destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
758 refine (X_ ((update_xi ξ t (leaves varstypes)))
759 (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
765 inversion X; subst; clear X.
767 apply (@ELetRec _ _ _ _ _ _ _ varstypes).
769 apply (@letrec_helper Γ Δ t varstypes).
770 rewrite mapOptionTree_compose.
771 rewrite mapOptionTree_compose.
773 replace ((mapOptionTree unlev (y @@@ t))) with y.
775 clear pf1 X0 X1 pfdist pf2 vars varstypes.
776 induction y; try destruct a; auto.
785 apply ILeaf; simpl; intros.
792 (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
793 * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
794 rename Σ into body_freevars_types.
795 rename vars into all_freevars.
796 rename X0 into body_expr.
797 rename X into alts_exprs.
799 destruct all_freevars; try destruct o; inversion H.
800 rename all_freevars2 into body_freevars.
801 rename all_freevars1 into alts_freevars.
803 set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
804 set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
805 apply fix_indexing in alts_exprs'.
806 simpl in alts_exprs'.
807 apply unindex_tree in alts_exprs'.
808 simpl in alts_exprs'.
809 apply fix2 in alts_exprs'.
810 apply treeM in alts_exprs'.
812 refine ( alts_exprs' >>>= fun Y =>
814 >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
820 Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
821 match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
822 | scnd_weak _ => let case_nil := tt in fun _ => INone _ _
823 | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
824 | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
827 Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
828 FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
830 induction Σ; intro ξ.
833 set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
834 refine (q >>>= fun q' => return _).
837 destruct q' as [varstypes [pf1 [pf2 distpf]]].
838 exists (mapOptionTree (@fst _ _) varstypes).
839 exists (update_xi ξ l (leaves varstypes)).
844 refine (bind f1 = IHΣ1 ξ ; _).
846 destruct f1 as [vars1 [ξ1 pf1]].
847 refine (bind f2 = IHΣ2 ξ1 ; _).
849 destruct f2 as [vars2 [ξ2 pf22]].
851 exists (vars1,,vars2).
859 Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
860 {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
861 FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
863 set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
864 apply closed2expr in cnd.
868 refine (bind ξvars = manyFresh _ Σ ξ0; _).
870 destruct ξvars as [vars ξpf].
871 destruct ξpf as [ξ pf].
872 refine (cnd ξ vars _ >>>= fun it => _).
875 refine (return OK _).
883 End HaskProofToStrong.