proposition: Lemma Y_approx : forall P, demorgan_inductively_barred_at P -> forall l, approx (X P) l -> Y P l.
proof: Proof. intros P DeMorgan. 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 DeMorgan l' l Hl'); auto. * intro n. apply inductively_barred_at_imp_is_path_from. -- assumption. -- firstorder. Qed.
imports: WeakFan List Arith Compare_dec