proposition: Lemma inductively_barred_at_is_path_from_decidable : forall P, (forall l, P l \/ ~ P l) -> demorgan_inductively_barred_at P.
proof: Proof. intros P Hdec n l H. destruct (inductively_barred_at_decidable P Hdec n (true::l)). - destruct (inductively_barred_at_decidable P Hdec n (false::l)). + auto. + auto. - auto. Qed.
imports: WeakFan List Arith Compare_dec