proposition: Lemma refineFun_Proper {fDom : list Type} {fCod : Type} : Proper (refineEquivFun ==> refineEquivFun ==> iff) (@refineFun fDom fCod).
proof: Proof. unfold Proper, respectful, refineEquivFun; intros; intuition. rewrite H1, H0; eauto. rewrite H2, H0; 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