proposition: Lemma funMax_Proper {fDom : list Type} {fCod : Type} : Proper (@refineEquivFun fDom fCod ==> @refineEquivFun fDom fCod ==> @refineEquivFun fDom fCod) FunMax.
proof: Proof. unfold refineEquivFun, Proper, respectful; intuition. - induction fDom; simpl in *. + intros c Comp_v; destruct Comp_v. apply H0 in H; apply H2 in H4; constructor; eauto. + intros. eapply IHfDom; eauto. - induction fDom; simpl in *. + intros c Comp_v; destruct Comp_v. apply H1 in H; apply H3 in H4; constructor; 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