proposition: Theorem WeakFanTheorem : forall P, barred P -> inductively_barred P [].
proof: Proof. intros P Hbar. destruct Hbar with (X P) as (l,(Hd%Y_approx,HP)). assert (inductively_barred P l) by (apply (now P l), HP). clear Hbar HP. induction l as [|a l]. - assumption. - destruct Hd as (Hd,HX). apply (IHl Hd). clear IHl. destruct a; unfold X in HX; simpl in HX. + apply propagate; assumption. + exfalso; destruct (HX H). Qed.
imports: List