proposition: Lemma fun_eq_cast : forall f g m (ts : terms m) n (us : terms n) (p : m = arity f) (q : n = arity g) (r : m=n), f = g -> us = Vcast ts r -> Fun f (Vcast ts p) = Fun g (Vcast us q).
proof: Proof. destruct ts; intros. subst g. apply args_eq. destruct n. 2: discr. VOtac. assert (p=q). apply eq_unique. subst q. apply Vcast_eq_intro. auto. subst g. apply args_eq. destruct n0. discr. rewrite H0, Vcast_cast. assert (trans_eq r q = p). apply eq_unique. rewrite H. refl. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)