proposition: Lemma refineEquivFun_lift {fDom : list Type} {fCod : Type} : forall (f : (funType fDom fCod -> Prop) -> Prop), refineEquivFun (refineFun_lift fDom f) (Curry _ (refineFun_lift _ (fun p : funType (cons (unCurry_funType fDom) nil) fCod -> Prop => f (fun f' => p (unCurry _ f' ))))).
proof: Proof. induction fDom; simpl. - intros; split; reflexivity. - simpl; split; simpl; intros. destruct (IHfDom (fun f' => f (fun a' => f' (a' t)))); simpl in *. eapply H. destruct (IHfDom (fun f' => f (fun a' => f' (a' t)))); simpl in *. eapply H0. 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