proposition: Lemma apps_apps : forall p (ts : Tes p) t q (us : Tes q), apps (apps t ts) us = apps t (Vapp ts us).
proof: Proof. induction ts; fo. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)