proposition: Lemma omAx2 : forall X, Sinductive X -> Subq Som X.
proof: Proof. intros X H. apply ASubq_Subq_p1. cbn. rewrite <- CR1. apply AomAx2. now apply Ainductive_Sinductive. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms