Predeclared theorems:

Some of these are redundant and retained mainly for backward compatibility.

CASEINTRO:

?x = ?y || ?x , ?x

COMP:

(?f @@ ?g) @ ?x = ?f @ ?g @ ?x

EQUATION:

?a = ?b = (?a = ?b) || true , false

FNDIST:

?f @ ?x || ?y , ?z = ?x || (?f @ ?y) , ?f @ ?z

HYP:

(?a = ?b) || (?f @ ?a) , ?c = (?a = ?b) || (?f @ ?b) , ?c

Id:

Id @ ?x = ?x

NONTRIV:

true = false = false

ODDCHOICE:

?x = ?x This theorem originally had a different form which is now not a permitted form for a theorem (and is automatically executed by the prover). It is present to avoid the necessity of editing it out of old files.

P1:

P1 @ ?x , ?y = ?x

P2:

P2 @ ?x , ?y = ?y

p1:

p1 @ ?x , ?y = ?x

p2:

p2 @ ?x , ?y = ?y

REFLEX:

?a = ?a = true

TYPES:

?t : ?t : ?x = ?t : ?x