proposition: Lemma is_path_from_imp_inductively_barred_at : forall P n l, is_path_from P n l -> inductively_barred_at P n l -> False.
proof: Proof. intros P; induction n; intros l H1 H2. - inversion_clear H1. inversion_clear H2. auto. - inversion_clear H1. + inversion_clear H2. * auto. * apply IHn with (true::l); auto. + inversion_clear H2. * auto. * apply IHn with (false::l); auto. Qed.
imports: WeakFan List Arith Compare_dec