proposition: Lemma class_eq X X' s s' : Aeq s s' -> class X s -> class X' s' -> X = X'.
proof: Proof. Proof using ce. destruct X as [P HP], X' as [P' HP']; simpl. intros H1 H2 XX. assert (H : P = P'). - destruct HP as [t ->], HP' as [t' ->]. apply ce. intros u. rewrite H2, H1, XX. tauto. - subst P'. now rewrite (PI HP HP'). Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)