proposition: Lemma Ainductive_Sinductive X : Ainductive (proj1_sig X) <-> Sinductive X.
proof: Proof. split; intros [H1 H2]; split. - now apply Ain_IN_NS_p1. - intros Y H % IN_Ain_p1. apply H2 in H. unfold IN. cbn. now rewrite <- !CR1. - now apply IN_Ain_NS_p1. - intros s H % Ain_IN_NS_p1. specialize (H2 (NS s) H). unfold IN in H2. cbn in H2. now rewrite <- !CR1 in H2. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms