proposition: Lemma tapp_typed (u v w: trace): tapp u v w -> forall n m p, typed n m u -> typed m p v -> typed n p w.
proof: Proof. induction 1; intros n m p Hu Hv. now inversion_clear Hu. now inversion_clear Hu. inversion_clear Hu. constructor. eapply IHtapp; eassumption. Qed.
imports: prop monoid positives comparisons