proposition: Lemma inductively_barred_at_decidable : forall P, (forall l, P l \/ ~ P l) -> forall n l, inductively_barred_at P n l \/ ~ inductively_barred_at P n l.
proof: Proof. intros P HP. induction n; intros. - destruct (HP l). + left. apply now_at, H. + right. inversion 1. auto. - destruct (HP l). + left. apply now_at, H. + destruct (IHn (true::l)). * destruct (IHn (false::l)). { left. apply propagate_at; assumption. } { right. inversion_clear 1; auto. } * right. inversion_clear 1; auto. Qed.
imports: WeakFan List Arith Compare_dec