proposition: Lemma caeq_inv : forall f n (ts : Tes n) g p (us : Tes p), caeq (mk_call f ts) (mk_call g us) -> exists f0 n0 (ts1 us1 : Tes n0), ts1 ~~~ us1 /\ f0 = f /\ n0 = n /\ existT ts1 = existT ts /\ f = g /\ n = p /\ existT us1 = existT us.
proof: Proof. intros f n ts g p us e. inversion e; clear e; subst. ex g p ts1 us1. fo. Qed.
imports: Coq(Morphisms Basics Lexicographic_Product) CoLoR(LogicUtil LSimple VecUtil RelUtil VecOrd EqUtil Lexico SN NatUtil)