proposition: Lemma min_eq : forall R t, min (red R) t <-> (forall f ts, t = Fun f ts -> Vforall (fun u => ~NT (red R) u) ts).
proof: Proof. intros R t. split. intros ht f ts e. apply Vforall_intro. intros u hu. apply ht. subst. apply subterm_fun. hyp. intros h u ut hu. destruct ut as [c [hc e]]. destruct c. cong. clear hc. simpl in e. set (ts := Vcast (Vapp t0 (Vcons (fill c u) t1)) e0). fold ts in e. ded (h f ts e). assert (Vin (fill c u) ts). unfold ts. rewrite Vin_cast. apply Vin_app_cons. assert (NT (red R) (fill c u)). destruct hu as [g [g0 hg]]. exists (fun k => fill c (g k)). rewrite g0. split_all. intro k. apply red_fill. apply hg. ded (Vforall_in H H0). contr. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)