proposition: Lemma eq_apps_fun_head : forall f p (ts : Tes p) g q (us : Tes q), apps (Fun f) ts = apps (Fun g) us -> f = g.
proof: Proof. intros f p ts g q us e. gen (f_equal head e). rewrite !head_apps. simpl. intro a. inversion a. refl. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)