proposition: Lemma omAx1 : Sinductive Som.
proof: Proof. split. - apply Ain_IN_NS. apply AomAx1. - intros X H. unfold IN in *; cbn in *. rewrite <- !CR1 in *. now apply AomAx1. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms