proposition: Lemma FST_FSTeq rho : rho ⊫ FSTeq.
proof: Proof. intros phi [<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]; cbn -[Aunion]. - apply Aeq_ref. - apply Aeq_sym. - apply Aeq_tra. - intros s t s' t' -> ->. tauto. - apply Aeq_ext. - apply AEmptyAx. - intros X Y Z. rewrite AunionAx. split; intros H. + destruct H as [A[H1 H2]]. apply AupairAx in H1 as [H1|H1]. * left. rewrite H1 in H2. apply AupairAx in H2. tauto. * right. rewrite <- H1. tauto. + destruct H as [H|H]. * exists (Aupair Y Y). rewrite !AupairAx. intuition. * exists X. split; trivial. apply AupairAx. now right. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Deduction.FullNDFacts ZF FST) Undecidability.FOL.Sets(Models.Aczel Models.ZF_model ZF minZF FST) Undecidability.FOL.Reductions(PCPb_to_ZF PCPb_to_ZFeq PCPb_to_minZF PCPb_to_minZFeq PCPb_to_ZFD) Lia Undecidability.PCP(PCP) Undecidability(Shared.ListAutomation)