proposition: Lemma fun_eq_intro : forall f ts g us (h : f = g), us = Vcast ts (f_equal (@arity Sig) h) -> Fun f ts = Fun g us.
proof: Proof. intros. rewrite <- (Vcast_refl ts (eq_refl (arity f))), <- (Vcast_refl us (eq_refl (arity g))). eapply fun_eq_cast. hyp. apply H. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)