proposition: Lemma refineFunEquiv_Curry (fDom : list Type) {fCod : Type} : forall (f : funType (cons (unCurry_funType fDom) nil) fCod), refineEquivFun f (unCurry _ (Curry _ f)).
proof: Proof. induction fDom; simpl. - split; simpl; intros; destruct t; apply PreOrder_Reflexive. - simpl in *; split; simpl; intros. + destruct t; simpl in *. eapply (IHfDom (fun u => f (a0, u))). + destruct t; simpl in *. eapply (IHfDom (fun u => f (a0, u))). 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