proposition: Theorem height_pred_not_nil2 : forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)), height_pred n ln l t -> l <> [].
proof: Proof. intros n ln t l H; elim H; simpl in |- *; auto. intros; discriminate. intros n0 ln1 ln2 t1 t2 l1 l2 H0; case l1; simpl in |- *; auto. intros; discriminate. Qed.
imports: Coq(ArithRing)