Welcome to Abella 2.0.5-dev

Abella < Define eq : A -> A -> prop by 
eq X X.

Abella < Type p A -> o.

Abella < Theorem eq_non_schm [A,B] : 
forall X Y, eq (p X) (p Y) -> false.

============================
 forall X Y, eq (p X) (p Y) -> false

eq_non_schm < intros.

Variables: X Y
H1 : eq (p X) (p Y)
============================
 false

eq_non_schm < skip.
Proof completed.

Abella < Theorem true_thm_with_no_schematic_proof [A,B] : 
forall X F, exists Y, eq (p X) (p Y) \/ (eq (p X) (p Y) -> false).

============================
 forall X F, exists Y, eq (p X) (p Y) \/ (eq (p X) (p Y) -> false)

true_thm_with_no_schematic_proof < skip.
Proof completed.

Abella <