proposition: Lemma refineFun_unCurry (fDom : list Type) {fCod : Type} : forall (f f' : funType fDom fCod), refineFun f f' -> refineFun (unCurry _ f) (unCurry _ f').
proof: Proof. induction fDom; simpl. - intros; eauto. - intros. eapply IHfDom; 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