proposition: Lemma model_replacement_comprehension: replacementA -> comprehensionA.
proof: Proof. move => h x p ux. have su:(forall t, U t -> R t x -> p t -> U t) by move => t. move: (h x p id ux su)=> [r [r1 r2]]; exists r; split => // z uz. split; first by move /(r2 _ uz)=> [t _ [ta tb ->]]. by move=> [pa pb]; apply /(r2 _ uz); exists z. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)