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`