proposition: Lemma eq_apps_fun_args : forall f p (ts : Tes p) g q (us : Tes q) (h : apps (Fun f) ts = apps (Fun g) us), ts = Vcast us (eq_apps_fun_nb_args_sym h).
proof: Proof. intros f p ts g q us h. assert (i : nb_args (Fun f) = nb_args (Fun g)). refl. gen (eq_apps_args h i); intro j. rewrite j at 1. apply Vcast_pi. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)