proposition: Lemma Y_approx : forall P l, approx (X P) l -> Y P l.
proof: Proof. induction l. - trivial. - intros (H,Hb). split. + auto. + unfold X in Hb. destruct a. * destruct Hb as (l',(Hl',(HYl',HY))). rewrite <- (Y_unique P l' l Hl'); auto. * firstorder. Qed.
imports: List