proposition: Lemma TD_CE_normaliser : CE -> TD -> inhabited extensional_normaliser.
proof: Proof. intros ce [delta H]. split. unshelve econstructor. - exact delta. - exact H. - intros P P' HP. now rewrite (ce _ _ HP). - intros s H1 H2. apply Aczel_CE.PI, ce. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts ZF) Undecidability.FOL.Sets(ZF binZF) Undecidability.FOL.Sets.Models(Aczel Aczel_CE Aczel_TD) Coq(Lia)