proposition: Lemma symb_arg_eq : forall f us g vs (h : f = g), Fun f us = Fun g vs -> vs = Vcast us (f_equal (@arity Sig) h).
proof: Proof. intros. assert (q' : arity f = arity g). rewrite h; auto. assert (H1 : (Vcast us q') = (Vcast us (f_equal (@arity Sig) h))). apply Vcast_pi. gen (fun_eq_intro us h H1). intro. rewrite H0 in H. gen (fun_eq H). intro T; rewrite <- T. apply Vcast_pi. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)