proposition: Lemma app_apps : forall n (us : Tes n) u v, App (apps u us) v = apps u (Vadd us v).
proof: Proof. induction us; intros u v. refl. simpl Vadd. simpl apps. apply IHus. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)