proposition: Lemma lub_refineFun_sup (fDom : list Type) {fCod : Type} (f : funType fDom fCod -> Prop) : lub f (refineFun_sup f).
proof: Proof. unfold refineFun_sup. unfold lub; split. - simpl; intros. rewrite refineEquivFun_lift; simpl. etransitivity. eapply refineFunEquiv_unCurry. eapply refineFun_Curry'. simpl; unfold refine, computes_to; intros; eauto. - simpl; intros. etransitivity; [ eapply refineEquivFun_lift | eapply refineFun_unCurry' ]. simpl; intros. etransitivity. eapply (proj1 (refineFunEquiv_Curry _ _)). simpl. unfold refine, computes_to; intros. eapply H in H1. eapply (refineFun_unCurry _ _ _ H1); eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Sets.Ensembles Coq.ZArith.ZArith Coq.Classes.Morphisms Coq.Classes.SetoidTactics Fiat.Computation Fiat.Computation.SetoidMorphisms Coq.Logic.FunctionalExtensionality