proposition: Lemma non_confusion2 : forall t u π, t·u·π <> π.
proof: Proof. intros t u π. revert t u. induction π. discriminate. intros t u Habs. inversion Habs. subst t. apply (IHπ _ _ H1). Qed.
imports: ClassicalRealizability.Tactics