proposition: Lemma FunMin_ok {fDom : list Type} {fCod : Type} : forall l r : funType fDom fCod, PreO.min (le := refineFun) l r (FunMin l r).
proof: Proof. constructor. - induction fDom; simpl in *. + intros v Comp_v; econstructor; eauto. + eauto. - induction fDom; simpl in *. + intros v Comp_v; econstructor 2; eauto. + eauto. - induction fDom; simpl in *. + intros. intros v Comp_v; destruct Comp_v. * apply H; eauto. * apply H0; 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