Subst

Subst

Paradigm(s)	Declarative
Designed by	User:Hakerh400
Appeared in	2025
Computational class	Turing complete
Major implementations	Implemented
File extension(s)	.txt

Subst is an interactive theorem prover invented by User:Hakerh400 and documented in 2025.

Overview

Subst uses non-depended type theory with higher-order logic and implicit type polymorphism. It has only two inference rules: elimination of implication and elimination of universal quantifier. Subst supports computation and the main mechanisms for proving theorems are substitution, simplification and computation. Even though higher-order unification is uncomputable in the general case, Subst supports a wide range of higher-order unification schemes. Its substitution abilities are much richer than other theorem provers.

There are types, terms and proofs. Each term has a type and each proof has a statement. Statement is a term whose type is Prop (the type of logical propositions).

Types

The only built-in types are Prop and -> (the type of functions). User can declare a new type using keyword type. For example:

type Set 0

The command above declares a new type whose name is Set. The natural number (here 0) represents the number of type parameters. Type Prop has no type parameters, and type -> has two type parameters.

Terms

There are only two built-in terms: imp (implication) whose type is Prop -> Prop -> Prop, and univ (universal quantifier) whose type is (a -> Prop) -> Prop for any type a (univ is polymorphic in type a).

There are two ways to introduce a term: const (for constants) and def (for definition). The difference is that a constant is completely opaque, while a definition has a definitional theorem that describes how the term is defined.

Examples of constants:

const mem : Set -> Set -> Prop
const tau : (a -> Prop) -> a

Term mem represents the set membership relation. It takes two sets and returns a proposition indicating whether the first set belongs to the second set. Term tau represents the choice function, sometimes called Hilbert's classical epsilon operator. It takes a predicate over some type a and returns a value of type a that satisfies the predicate if it exists, or any value of the given type otherwise. Note that both mem and tau are introduced as constants, so they have no meaning without appropriate axioms describing them.

Before we show definitions, it is worth mentioning that Subst has no built-in operators, but operators are not defined in the source code either. Instead, they are stored in a separate file. The format of that file will not be explained here. Lambda abstraction is represented as \, Universal quantifier is uppercase V, implication is -> (same symbol as function type), negation is -, disjunction is \/, conjunction is /\ and equivalence is <->. Binder TAU corresponds to the term tau. Operator # is right-associative low-precedence application operator. Inline comments start with ; or --.

Here are some definitions of propositional logic:

def T := TAU P, P
def F := TAU P, P -> V Q, Q
def not := \P, P -> F
def or := \P Q, -P -> Q
def and := \P Q, -(-P \/ -Q)
def iff := \P Q, (P -> Q) /\ (Q -> P)
def eq := \a b, V P, P a -> P b

True is defined as some proposition P such that P holds, if it exists. That is, some proposition that is provable, if it exists. False is defined as some proposition that implies all propositions, if it exists. Relations not, or, and and iff should be obvious. Equality between objects a and b holds iff any predicate P that holds for a also holds for b (note that types are implicit, equality has one type parameter).

For each definition, a corresponding definitional theorem is introduces as well. For example, definition def B := A creates a definitional theorem named B_def whose statement is V P, P B -> P A.

Axioms

There are two ways to introduce a global proof: axiom and thm (theorem). Here are examples of axioms:

axiom ax_k : V P Q, P -> Q -> P
axiom ax_s : V P Q R, (P -> Q -> R) -> (P -> Q) -> P -> R
axiom tau_spec : V P x, P x -> P (TAU y, P y)
axiom prop_ext : V P, P T -> P F -> V Q, P Q
axiom fn_ext : V f g, (V x, f x = g x) -> f = g

The first two axioms are from propositional logic and it should be obvious what they mean. Axiom tau_spec describes how TAU works. It says that for any predicate P and any term x, if P holds for x, then P also holds for tau P. Note that tau P is equivalent to TAU y, P y. Axiom prop_ext says that if something holds for true and false, then it holds for all propositions (classical logic). Axiom fn_ext is the standard function extensionality.

Theorems

Example:

thm 1 : V P, P -> TAU P, P := tau_spec \P, P

Keyword thm represents a theorem. Here 1 is the theorem name (yes, it can be a number as well). Then a colon : appears. After that we write the statement of the theorem, in this case that for any proposition P, if P holds, then TAU P, P also holds. After that, the := appears and then a proof.

A proof starts with a global proof name, in this case global axiom tau_spec. Then, if the statement of that proof starts with universal quantifier, a term is parsed and it represents elimination of universal quantifier. Otherwise, if the statement of the global proof is an implication, then another global proof name is parsed and it represents elimination of implication. In case of universal quantifier elimination, types must match. In case of implication elimination, both types and statements must match. If a type or term mismatch happens, it is a syntax error.

In this case, the statement V P, P -> TAU P, P is proved by universal quantifier elimination of tau_spec (whose statement is V P x, P x -> P (TAU y, P y)) with term \P, P. The final proof statement matches the statement mentioned in the theorem (up to alpha, beta and eta reduction), so it is a valid proof.

Here are more proofs:

thm 2 : (V P Q, P -> Q -> P) -> TAU P, P := 1 V P Q, P -> Q -> P
thm 3 : TAU P, P := 2 ax_k
thm 4 : (T -> (TAU P, P) -> T) -> (TAU P, P) -> (TAU P, P) -> T :=
  T_def \P, P -> (TAU P, P) -> T
thm 5 : V P, T -> P -> T := ax_k T
thm 6 : T -> (TAU P, P) -> T := 5 TAU P, P
thm 7 : (TAU P, P) -> (TAU P, P) -> T := 4 6
thm 8 : (TAU P, P) -> T := 7 3
thm triv : T := 8 3

thm 31 : T -> F -> T := 5 F
thm F_imp_T : F -> T := 31 triv
thm 33 : V P, F -> P -> F := ax_k F
thm 34 : F -> F -> F := 33 F
thm 35 : F -> (F -> F) -> F := 33 F -> F
thm 36 : V P Q, (F -> P -> Q) -> (F -> P) -> F -> Q := ax_s F
thm 37 : V P, (F -> (F -> F) -> P) -> (F -> F -> F) -> F -> P := 36 F -> F
thm 38 : (F -> (F -> F) -> F) -> (F -> F -> F) -> F -> F := 37 F
thm 39 : (F -> F -> F) -> F -> F := 38 35
thm F_imp_F : F -> F := 39 34
thm 41 : (F -> T) -> (F -> F) -> V P, F -> P := prop_ext \P, F -> P
thm 42 : (F -> F) -> V P, F -> P := 41 F_imp_T
thm of_F : V P, F -> P := 42 F_imp_F

thm 43 : (T -> T) -> (F -> F) -> V P, P -> P := prop_ext \P, P -> P
thm 44 : T -> T -> T := 5 T
thm T_imp_T : T -> T := 44 triv
thm 46 : (F -> F) -> V P, P -> P := 43 T_imp_T
thm imp_refl : V P, P -> P := 46 F_imp_F

thm 47 : (-F -> -F) -> (F -> F) -> -F := not_def \f, f F -> -F
thm 48 : -F -> -F := imp_refl -F
thm 49 : (F -> F) -> -F := 47 48
thm not_F : -F := 49 F_imp_F

thm 50 : (V P, P T -> P (TAU P, P)) -> V P, P (TAU P, P) -> P (TAU P, P) :=
  T_def \x, V P, P x -> P (TAU P, P)
thm 51 : (V P, P T -> P (TAU P, P)) -> V P, P (TAU P, P) -> P (TAU P, P) :=
  T_def \x, V P, P x -> P (TAU P, P)
thm 52 : V P, P (TAU P, P) -> P (TAU P, P) := 51 T_def

thm 53 : (V P, P F -> P (TAU P, P -> V Q, Q)) ->
  V P, P (TAU P, P -> V Q, Q) -> P (TAU P, P -> V Q, Q) :=
  F_def \x, V P, P x -> P (TAU P, P -> V Q, Q)
thm 54 : (V P, P F -> P (TAU P, P -> V Q, Q)) ->
  V P, P (TAU P, P -> V Q, Q) -> P (TAU P, P -> V Q, Q) :=
  F_def \x, V P, P x -> P (TAU P, P -> V Q, Q)
thm 55 : V P, P (TAU P, P -> V Q, Q) -> P (TAU P, P -> V Q, Q) := 54 F_def

thm 56 : T = T -> F = F -> V (P : Prop), P = P := prop_ext \x, x = x
thm 57 : (T = T -> F = F -> V (P : Prop), P = P) -> (V P, P T -> P T) ->
  F = F -> V (P : Prop), P = P :=
  eq_def \f, f T T -> F = F -> V (P : Prop), P = P
thm 58 : (V P, P T -> P T) -> F = F -> V (P : Prop), P = P := 57 56
thm 59 : ((V P, P T -> P T) -> F = F -> V (P : Prop), P = P) ->
  (V P, P (TAU P, P) -> P (TAU P, P)) -> F = F -> V (P : Prop), P = P :=
  T_def \x, (V P, P x -> P x) -> F = F -> V (P : Prop), P = P
thm 60 : (V P, P (TAU P, P) -> P (TAU P, P)) -> F = F -> V (P : Prop), P = P := 59 58
thm 61 : F = F -> V (P : Prop), P = P := 60 52
thm 62 : (F = F -> V (P : Prop), P = P) -> (V P, P F -> P F) -> V (P : Prop), P = P :=
  eq_def \f, f F F -> V (P : Prop), P = P
thm 63 : (V P, P F -> P F) -> V (P : Prop), P = P := 62 61
thm 64 : ((V P, P F -> P F) -> V (P : Prop), P = P) ->
  (V P, P (TAU P, P -> V Q, Q) -> P (TAU P, P -> V Q, Q)) -> V (P : Prop), P = P :=
  F_def \x, (V P, P x -> P x) -> V (P : Prop), P = P
thm 65 : (V P, P (TAU P, P -> V Q, Q) -> P (TAU P, P -> V Q, Q)) ->
  V (P : Prop), P = P := 64 63

thm prop_eq_refl : V (P : Prop), P = P := 65 55
thm T_eq_T : T = T := prop_eq_refl T
thm F_eq_F : F = F := prop_eq_refl F

thm 66 : V P, T = T -> P -> T = T := ax_k T = T
thm 67 : T = T -> T -> T = T := 66 T
thm 68 : T -> T = T := 67 T_eq_T
thm 69 : F -> F = T := of_F F = T
thm 70 : (T -> T = T) -> (F -> F = T) -> V P, P -> P = T :=
  prop_ext \x, x -> x = T
thm 71 : (F -> F = T) -> V P, P -> P = T := 70 68
thm eq_T_of : V P, P -> P = T := 71 69

thm 73 : T = T -> (T -> T) -> T = T := 66 T -> T
thm 77 : (T -> T) -> T = T := 73 T_eq_T
thm 78 : V P, F = F -> P -> F = F := ax_k F = F
thm 79 : F = F -> (F -> F) -> F = F := 78 F -> F
thm 80 : (F -> F) -> F = F := 79 F_eq_F
thm 81 : V P, ((F -> F) -> F = F) -> P -> (F -> F) -> F = F :=
  ax_k (F -> F) -> F = F
thm 82 : ((F -> F) -> F = F) -> (F -> F) -> (F -> F) -> F = F :=
  81 F -> F
thm 83 : (F -> F) -> (F -> F) -> F = F := 82 80

thm 84 : T -> (T -> F) -> T := 5 T -> F
thm 85 : (T -> F) -> T := 84 triv
thm 86 : V P Q, ((T -> F) -> P -> Q) ->
  ((T -> F) -> P) -> (T -> F) -> Q := ax_s T -> F
thm 87 : V P, ((T -> F) -> T -> P) ->
  ((T -> F) -> T) -> (T -> F) -> P := 86 T
thm 88 : ((T -> F) -> T -> F) ->
  ((T -> F) -> T) -> (T -> F) -> F := 87 F
thm 89 : (T -> F) -> T -> F := imp_refl T -> F
thm 90 : ((T -> F) -> T) -> (T -> F) -> F := 88 89
thm 91 : (T -> F) -> F := 90 85
thm 92 : ((T -> F) -> T) -> ((T -> F) -> F) -> V P, (T -> F) -> P :=
  prop_ext \x, (T -> F) -> x
thm 93 : ((T -> F) -> F) -> V P, (T -> F) -> P := 92 85
thm 94 : V P, (T -> F) -> P := 93 91

thm 95 : V P, ((T -> T) -> T = T) -> P -> (T -> T) -> T = T :=
  ax_k (T -> T) -> T = T
thm 96 : ((T -> T) -> T = T) -> (T -> T) -> (T -> T) -> T = T :=
  95 T -> T
thm 97 : (T -> T) -> (T -> T) -> T = T := 96 77
thm 98 : (T -> F) -> (F -> T) -> T = F := 94 (F -> T) -> T = F
thm 99 : (T -> F) -> F = T := 94 F = T
thm 100 : V P, ((T -> F) -> F = T) -> P -> (T -> F) -> F = T :=
  ax_k (T -> F) -> F = T
thm 101 : ((T -> F) -> F = T) -> (F -> T) -> (T -> F) -> F = T :=
  100 F -> T
thm 102 : (F -> T) -> (T -> F) -> F = T := 101 99

thm 103 : ((T -> T) -> (T -> T) -> T = T) -> ((T -> F) -> (F -> T) -> T = F) ->
  V P, (T -> P) -> (P -> T) -> T = P :=
  prop_ext \x, (T -> x) -> (x -> T) -> T = x
thm 104 : ((T -> F) -> (F -> T) -> T = F) ->
  V P, (T -> P) -> (P -> T) -> T = P := 103 97
thm 105 : V P, (T -> P) -> (P -> T) -> T = P := 104 98
thm 106 : ((F -> T) -> (T -> F) -> F = T) -> ((F -> F) -> (F -> F) -> F = F) ->
  V P, (F -> P) -> (P -> F) -> F = P :=
  prop_ext \x, (F -> x) -> (x -> F) -> F = x
thm 107 : ((F -> F) -> (F -> F) -> F = F) ->
  V P, (F -> P) -> (P -> F) -> F = P := 106 102
thm 108 : V P, (F -> P) -> (P -> F) -> F = P := 107 83
thm 109 : (V Q, (T -> Q) -> (Q -> T) -> T = Q) ->
  (V Q, (F -> Q) -> (Q -> F) -> F = Q) ->
  V P Q, (P -> Q) -> (Q -> P) -> P = Q :=
  prop_ext \x, V P, (x -> P) -> (P -> x) -> x = P
thm 110 : (V Q, (F -> Q) -> (Q -> F) -> F = Q) ->
  V P Q, (P -> Q) -> (Q -> P) -> P = Q := 109 105
thm eq_of_imp_imp : V P Q, (P -> Q) -> (Q -> P) -> P = Q := 110 108

thm 111 : V P, (T -> P) -> (P -> T) -> T = P := eq_of_imp_imp T
thm 112 : (T -> T = T) -> (T = T -> T) -> T = (T = T) := 111 T = T
thm 113 : (T = T -> T) -> T = (T = T) := 112 68
thm 114 : T -> T = T -> T := 5 T = T
thm 115 : T = T -> T := 114 triv
thm 116 : T = (T = T) := 113 115
thm 117 : V P, (F -> P) -> (P -> F) -> F = P := eq_of_imp_imp F

thm 120 : (T -> T) -> (T -> T) = T := eq_T_of T -> T
thm 121 : (T -> T) = T := 120 T_imp_T
thm 122 : (F -> F) -> (F -> F) = T := eq_T_of F -> F
thm 123 : (F -> F) = T := 122 F_imp_F
thm 124 : (T -> T) = T -> (F -> F) = T -> V P, (P -> P) = T :=
  prop_ext \x, (x -> x) = T
thm 125 : (F -> F) = T -> V P, (P -> P) = T := 124 121
thm 126 : V P, (P -> P) = T := 125 123
thm 127 : V f, (V P, (P -> P) = f P) -> (\P, P -> P) = f :=
  fn_ext \P, P -> P
thm 128 : (V P, (P -> P) = T) -> (\P, P -> P) = (\P, T) := 127 \P, T
thm 129 : (\P, P -> P) = (\P, T) := 128 126
thm 130 : (\P, P -> P) = (\P, T) -> V Q, Q (\P, P -> P) -> Q (\P, T) :=
  eq_def \x, x (\P, P -> P) (\P, T)
thm imp_refl_rw : V Q, Q (\P, P -> P) -> Q (\P, T) := 130 129

Simplification

A simplification reduction rule can be introduced by pragma add_simp <theorem name>. For example:

pragma add_simp imp_refl_rw

It means that if a proof of any subsequent theorem is an elimination of universal quantifier, whenever P -> P appears in the statement, for any proposition P, it will be replaced with T. Here are more proofs:

thm 132 : T = T -> (T = T) = T := eq_T_of T = T
thm 133 : (T = T) = T := 132 T_eq_T
thm 134 : F = F -> (F = F) = T := eq_T_of F = F
thm 135 : (F = F) = T := 134 F_eq_F
thm 136 : (T = T) = T -> (F = F) = T -> V (P : Prop), (P = P) = T :=
  prop_ext \x, (x = x) = T
thm 137 : (F = F) = T -> V (P : Prop), (P = P) = T := 136 133
thm 138 : V (P : Prop), (P = P) = T := 137 135
thm 139 : V f, (V P, (P = P) = f P) -> (\P, P = P) = f :=
  fn_ext \x, x = x
thm 140 : (V (P : Prop), (P = P) = T) -> (\(P : Prop), P = P) = (\P, T) :=
  139 \(P : Prop), T
thm 141 : (\(P : Prop), P = P) = (\P, T) := 140 138
thm 142 : (\(P : Prop), P = P) = (\P, T) ->
  V Q, Q (\(P : Prop), P = P) -> Q (\P, T) :=
  eq_def \x, x (\(P : Prop), P = P) (\P, T)
thm prop_eq_refl_rw : V Q, Q (\(P : Prop), P = P) -> Q (\P, T) := 142 141
pragma add_simp prop_eq_refl_rw

thm 148 : T -> (V Q, Q T -> Q (TAU P, P)) -> V (Q : Prop -> Prop), T :=
  T_def \x, (V Q, Q T -> Q x) -> V Q, Q T -> Q T
thm 149 : (V Q, Q T -> Q (TAU P, P)) -> V (Q : Prop -> Prop), T := 148 triv
thm 150 : V (Q : Prop -> Prop), T := 149 T_def

thm 154 : (F -> T) -> (F -> T) = T := eq_T_of F -> T
thm 155 : (F -> T) = T := 154 F_imp_T
thm 158 : (F -> T) = T -> T -> V P, (F -> P) = T :=
  prop_ext \x, (F -> x) = T
thm 159 : T -> V P, (F -> P) = T := 158 155
thm 160 : V P, (F -> P) = T := 159 triv

thm 161 : V f, (V P, (F -> P) = f P) -> (\P, F -> P) = f :=
  fn_ext \x, F -> x
thm 162 : (V P, (F -> P) = T) -> (\P, F -> P) = (\P, T) :=
  161 \x, T
thm 163 : (\P, F -> P) = (\P, T) := 162 160
thm 164 : ((\P, F -> P) = (\P, T)) -> V Q, Q (\P, F -> P) -> Q (\P, T) :=
  eq_def \x, x (\P, F -> P) (\P, T)
thm F_imp_rw : V Q, Q (\P, F -> P) -> Q (\P, T) := 164 163
pragma add_simp F_imp_rw

thm 171 : (V (Q : Prop -> Prop), T) -> (V (Q : Prop -> Prop), T) ->
  V P Q, (P -> Q P) = (P -> Q T) := prop_ext \x,
  V Q, (x -> Q x) = (x -> Q T)
thm 172 : (V (Q : Prop -> Prop), T) -> V P Q, (P -> Q P) = (P -> Q T) :=
  171 150
thm 173 : V P Q, (P -> Q P) = (P -> Q T) := 172 150

thm 174 : V f, (V Q, (T -> Q T) = f Q) -> (\Q, T -> Q T) = f :=
  fn_ext \x, T -> x T
thm 175 : (V (Q : Prop -> Prop), T) -> (\Q, T -> Q T) = (\Q, T -> Q T) :=
  174 \x, T -> x T
thm 176 : (\Q, T -> Q T) = (\Q, T -> Q T) := 175 150
thm 177 : V f, (V Q, T = f Q) -> (\(Q : Prop -> Prop), T) = f :=
  fn_ext \x, F -> x F
thm 178 : (V (Q : Prop -> Prop), T) -> (\(Q : Prop -> Prop), T) = (\(Q : Prop -> Prop), T) :=
  177 \x, F -> x T
thm 179 : (\(Q : Prop -> Prop), T) = (\(Q : Prop -> Prop), T) := 178 150

thm 500 : (\(R : Prop -> Prop), T) = (\R, T) ->
  ((\(R : Prop -> Prop), T) = (\R, T)) = T :=
  eq_T_of (\(R : Prop -> Prop), T) = (\R, T)
thm 501 : ((\(R : Prop -> Prop), T) = (\R, T)) = T := 500 179
thm 502 : ((\(R : Prop -> Prop), T) = (\R, T)) = T -> V Q,
  Q ((\(R : Prop -> Prop), T) = (\R, T)) -> Q T :=
  eq_def \f, f ((\(R : Prop -> Prop), T) = (\R, T)) T
thm 503 : V Q, Q ((\(R : Prop -> Prop), T) = (\R, T)) -> Q T := 502 501
pragma add_simp 503

thm 180 : (\Q, T -> Q T) = (\Q, T -> Q T) ->
  T -> V P, (\Q, P -> Q P) = (\Q, P -> Q T) := prop_ext \P,
  (\Q, P -> Q P) = (\Q, P -> Q T)
thm 181 : T -> V P, (\Q, P -> Q P) = (\Q, P -> Q T) := 180 176
thm 182 : V P, (\Q, P -> Q P) = (\Q, P -> Q T) := 181 triv
thm 183 : V f, (V P, (\Q, P -> Q P) = f P) -> (\P Q, P -> Q P) = f :=
  fn_ext \x Q, x -> Q x
thm 184 : (V P, (\Q, P -> Q P) = (\Q, P -> Q T)) ->
  (\P Q, P -> Q P) = (\P Q, P -> Q T) :=
  183 \x Q, x -> Q T
thm 185 : (\P Q, P -> Q P) = (\P Q, P -> Q T) := 184 182

thm 186 : ((\P Q, P -> Q P) = (\P Q, P -> Q T)) ->
  V R, R (\P Q, P -> Q P) -> R (\P Q, P -> Q T) :=
  eq_def \f, f (\P Q, P -> Q P) (\P Q, P -> Q T)
thm imp_pos_rw : V R, R (\P Q, P -> Q P) -> R (\P Q, P -> Q T) := 186 185

thm 188 : V P, ((T -> F) -> P) -> (P -> T -> F) -> (T -> F) = P :=
  eq_of_imp_imp T -> F
thm 189 : ((T -> F) -> F) -> T -> (T -> F) = F := 188 F
thm 190 : T -> (T -> F) = F := 189 91
thm 192 : (T -> F) = F := 190 triv
thm 193 : T -> (T -> F) = F -> V P, (T -> P) = P :=
  prop_ext \P, (T -> P) = P
thm 194 : (T -> F) = F -> V P, (T -> P) = P := 193 triv
thm 195 : V P, (T -> P) = P := 194 192
thm 196 : V f, (V P, (T -> P) = f P) -> (\P, T -> P) = f :=
  fn_ext \ P, T -> P
thm 197 : (V P, (T -> P) = P) -> (\P, T -> P) = (\P, P) := 196 \P, P
thm 198 : (\P, T -> P) = (\P, P) := 197 195
thm 199 : ((\P, T -> P) = (\P, P)) -> V Q, Q (\P, T -> P) -> Q (\P, P) :=
  eq_def \f, f (\P, T -> P) (\P, P)
thm T_imp_rw : V Q, Q (\P, T -> P) -> Q (\P, P) := 199 198
pragma add_simp T_imp_rw

thm imp_T : V P, P -> T := ax_k F -> V Q, Q F -> Q T
thm 207 : (V (Q : Prop -> Prop), T) -> T := imp_T V Q, F -> Q F -> Q T

thm 225 : V P, ((V (Q : Prop -> Prop), T) -> P) ->
  (P -> V (Q : Prop -> Prop), T) -> (V (Q : Prop -> Prop), T) = P :=
  eq_of_imp_imp V Q, F -> Q F -> Q T
thm 226 : ((V (Q : Prop -> Prop), T) -> T) -> (V (Q : Prop -> Prop), T) ->
  (V (Q : Prop -> Prop), T) = T := 225 F -> V Q, Q F -> Q T
thm 227 : (V (Q : Prop -> Prop), T) -> (V (Q : Prop -> Prop), T) = T
  := 226 207
thm 229 : (V (Q : Prop -> Prop), T) = T := 227 150

thm 417 : (V (Q : Prop -> Prop), T) = T ->
  V R, R (V (Q : Prop -> Prop), T) -> R T :=
  eq_def \f, f (V (Q : Prop -> Prop), T) T
thm 418 : V R, R (V (Q : Prop -> Prop), T) -> R T := 417 229
pragma add_simp 418

thm 232 : V P, (V Q, P -> Q F -> Q T) = (P -> V Q, Q F -> Q T) :=
  prop_ext \x, (V Q, x -> Q F -> Q T) = (x -> V Q, Q F -> Q T)
thm 233 : V f, (V P, (V Q, P -> Q F -> Q T) = f P) ->
  (\P, V Q, P -> Q F -> Q T) = f := fn_ext \P, V Q, P -> Q F -> Q T
thm 234 : (V P, (V Q, P -> Q F -> Q T) = (P -> V Q, Q F -> Q T)) ->
  (\P, V Q, P -> Q F -> Q T) = (\P, P -> V Q, Q F -> Q T) :=
  233 \P, P -> V Q, Q F -> Q T
thm 235 : (\P, V Q, P -> Q F -> Q T) = (\P, P -> V Q, Q F -> Q T) :=
  234 232
thm 236 : ((\P, V Q, P -> Q F -> Q T) = (\P, P -> V Q, Q F -> Q T)) ->
  V Q, Q (\P, V Q, P -> Q F -> Q T) -> Q (\P, P -> V Q, Q F -> Q T) :=
  eq_def \f, f (\P, V Q, P -> Q F -> Q T) (\P, P -> V Q, Q F -> Q T)
thm 237 : V Q, Q (\P, V Q, P -> Q F -> Q T) ->
  Q (\P, P -> V Q, Q F -> Q T) := 236 235

thm 118 : (F = T -> F) -> F = (F = T) := 117 F = T
thm 239 : F = T -> V Q, Q F -> Q T := eq_def \f, f F T
thm 240 : (F = T -> V Q, Q F -> Q T) -> V Q, F = T -> Q F -> Q T :=
  237 \x, x (F = T) -> V Q, F = T -> Q F -> Q T
thm 243 : V Q, F = T -> Q F -> Q T := 240 239
thm 244 : F = T -> F := 243 \x, x -> F
thm 249 : F = (F = T) := 118 244

thm 250 : F = (F = T) -> V P, P = (P = T) :=
  prop_ext \x, x = (x = T)
thm 252 : V P, P = (P = T) := 250 249
thm 253 : V f, (V P, P = f P) -> (\P, P) = f := fn_ext \x, x
thm 254 : (V P, P = (P = T)) -> (\P, P) = (\P, P = T) :=
  253 \x, x = T
thm 255 : (\P, P) = (\P, P = T) := 254 252
thm 256 : (\P, P) = (\P, P = T) -> V Q, Q (\P, P) -> Q (\P, P = T) :=
  eq_def \f, f (\P, P) (\P, P = T)
thm eq_T_rw' : V Q, Q (\P, P) -> Q (\P, P = T) := 256 255

thm 257 : (V P, P -> T) -> V P, (P -> T) = T :=
  eq_T_rw' \f, V P, f (P -> T)
thm 258 : V P, (P -> T) = T := 257 imp_T
thm 259 : V f, (V P, (P -> T) = f P) -> (\P, P -> T) = f :=
  fn_ext \x, x -> T
thm 260 : (V P, (P -> T) = T) -> (\P, P -> T) = (\P, T) :=
  259 \x, T
thm 261 : (\P, P -> T) = (\P, T) := 260 258
thm 262 : (\P, P -> T) = (\P, T) ->
  V Q, Q (\P, P -> T) -> Q (\P, T) :=
  eq_def \f, f (\P, P -> T) (\P, T)
thm imp_T_rw : V Q, Q (\P, P -> T) -> Q (\P, T) := 262 261
pragma add_simp imp_T_rw

thm 419 : V (P : Prop), T := prop_ext \x, T
thm 420 : (V (P : Prop), T) -> (V (P : Prop), T) = T :=
  eq_T_of V (P : Prop), T
thm 421 : (V (P : Prop), T) = T := 420 419
thm 422 : (V (P : Prop), T) = T ->
  V Q, Q (V (P : Prop), T) -> Q T := eq_def
  \f, f (V (P : Prop), T) T
thm 423 : V Q, Q (V (P : Prop), T) -> Q T := 422 421
pragma add_simp 423

thm 279 : V f, (V P, T = f P) ->
  (\(P : Prop), T) = f := fn_ext \x, T -> x -> T
thm 280 : (\(P : Prop), T) = (\P, T) := 279 \x, T
thm 281 : (\(P : Prop), T) = (\P, T) ->
  ((\(P : Prop), T) = (\P, T)) = T :=
  eq_T_of (\(P : Prop), T) = (\P, T)
thm 282 : ((\(P : Prop), T) = (\P, T)) = T := 281 280
thm 283 : ((\(P : Prop), T) = (\P, T)) = T ->
  V Q, Q ((\(P : Prop), T) = (\P, T)) -> Q T :=
  eq_def \f, f ((\(P : Prop), T) = (\P, T)) T
thm 284 : V Q, Q ((\(P : Prop), T) = (\P, T)) -> Q T :=
  283 282
pragma add_simp 284

thm 287 : V P, (\Q, P -> Q -> P) = (\Q, T) :=
  prop_ext \x, (\Q, x -> Q -> x) = (\Q, T)
thm 290 : V f, (V P, (\Q, P -> Q -> P) = f P) ->
  (\P Q, P -> Q -> P) = f := fn_ext \P Q, P -> Q -> P
thm 291 : (V P, (\Q, P -> Q -> P) = (\Q, T)) ->
  (\P Q, P -> Q -> P) = (\P Q, T) := 290 \P Q, T
thm 292 : (\P Q, P -> Q -> P) = (\P Q, T) := 291 287
thm 293 : (\P Q, P -> Q -> P) = (\P Q, T) ->
  V R, R (\P Q, P -> Q -> P) -> R (\P Q, T) :=
  eq_def \f, f (\P Q, P -> Q -> P) (\P Q, T)
thm ax_k_rw : V R, R (\P Q, P -> Q -> P) ->
  R (\P Q, T) := 293 292
pragma add_simp ax_k_rw

thm 297 : -F -> (-F) = T := eq_T_of -F
thm 298 : (-F) = T := 297 not_F
thm 299 : (-F) = T -> V Q, Q (-F) -> Q T :=
  eq_def \f, f (-F) T
thm not_F_rw : V Q, Q (-F) -> Q T := 299 298
pragma add_simp not_F_rw

thm 320 : V Q, (\R, R (Q -> F) -> R (-Q -> F) -> R F) = (\R, T) :=
  prop_ext \x, (\R, R (x -> F) -> R (-x -> F) -> R F) = (\R, T)
thm 323 : V f, (V Q, (\R, R (Q -> F) -> R (-Q -> F) -> R F) = f Q) ->
  (\Q R, R (Q -> F) -> R (-Q -> F) -> R F) = f :=
  fn_ext \Q R, R (Q -> F) -> R (-Q -> F) -> R F
thm 324 : (V Q, (\R, R (Q -> F) -> R (-Q -> F) -> R F) = (\R, T)) ->
  (\Q R, R (Q -> F) -> R (-Q -> F) -> R F) = (\Q R, T) :=
  323 \Q R, T
thm 326 : (\Q R, R (Q -> F) -> R (-Q -> F) -> R F) = (\Q R, T) :=
  324 320

thm 335 : V f, (V (Q : Prop), (\(R : Prop -> Prop), T) = f Q) ->
  (\(Q : Prop) (R : Prop -> Prop), T) = f :=
  fn_ext \(Q : Prop) (R : Prop -> Prop), T
thm 337 : (\(Q : Prop) (R : Prop -> Prop), T) = (\Q R, T) :=
  335 \Q R, T

thm 339 : (\(Q : Prop) (R : Prop -> Prop), T) = (\Q R, T) ->
  (\Q R, R (Q -> F) -> R (-Q -> F) -> R F) = (\Q R, T) ->
  V P, (\Q R, R (Q -> P) -> R (-Q -> P) -> R P) = (\Q R, T) :=
  prop_ext \x, (\Q R, R (Q -> x) -> R (-Q -> x) -> R x) = (\Q R, T)
thm 340 : (\Q R, R (Q -> F) -> R (-Q -> F) -> R F) = (\Q R, T) ->
  V P, (\Q R, R (Q -> P) -> R (-Q -> P) -> R P) = (\Q R, T) := 339 337
thm 341 : V P, (\Q R, R (Q -> P) -> R (-Q -> P) -> R P) = (\Q R, T) :=
  340 326
thm 342 : V f, (V P, (\Q R, R (Q -> P) -> R (-Q -> P) -> R P) = f P) ->
  (\P Q R, R (Q -> P) -> R (-Q -> P) -> R P) = f :=
  fn_ext \P Q R, R (Q -> P) -> R (-Q -> P) -> R P
thm 343 : (V P, (\Q R, R (Q -> P) -> R (-Q -> P) -> R P) = (\Q R, T)) ->
  (\P Q R, R (Q -> P) -> R (-Q -> P) -> R P) = (\P Q R, T) :=
  342 \P Q R, T
thm 344 : (\P Q R, R (Q -> P) -> R (-Q -> P) -> R P) = (\P Q R, T) :=
  343 341
thm 345 : (\P Q R, R (Q -> P) -> R (-Q -> P) -> R P) = (\P Q R, T) ->
  V S, S (\P Q R, R (Q -> P) -> R (-Q -> P) -> R P) -> S (\P Q R, T) :=
  eq_def \f, f (\P Q R, R (Q -> P) -> R (-Q -> P) -> R P) (\P Q R, T)
thm 346 : V S, S (\P Q R, R (Q -> P) -> R (-Q -> P) -> R P) ->
  S (\P Q R, T) := 345 344

thm univ_T : V x, T := tau_spec \x, T
thm 393 : (V (x : a), T) -> (V (x : a), T) = T := eq_T_of V x, T
thm 394 : (V x, T) = T := 393 univ_T
thm 395 : (V (x : a), T) = T -> V P, P (V (x : a), T) -> P T :=
  eq_def \f, f (V x, T) T
thm univ_T_rw : V P, P (V x, T) -> P T := 395 394
pragma add_simp univ_T_rw

thm 353 : V (P : a -> Prop), ((V y, P y) ->
  V x, (V y, P y) -> P x) -> (-(V y, P y) -> V x, (V y, P y) -> P x) ->
  V x, (V y, P y) -> P x := 346 \f,
  (V (P : a -> Prop), f (V x, (V y, P y) -> P x) (V y, P y) (\x, x)) ->
  V (P : a -> Prop), ((V y, P y) -> V x, (V y, P y) -> P x) ->
  (-(V y, P y) -> V x, (V y, P y) -> P x) -> V x, (V y, P y) -> P x
thm 354 : (V (P : a -> Prop), ((V y, P y) -> V x, (V y, P y) -> P x) ->
  (-(V y, P y) -> V x, (V y, P y) -> P x) -> V x, (V y, P y) -> P x) ->
  V (P : a -> Prop), (-(V y, P y) -> V x, (V y, P y) -> P x) ->
  V x, (V y, P y) -> P x := imp_pos_rw \f, V (P : a -> Prop),
  (f (V y, P y) # \z, V x, z -> P x) ->
  (-(V y, P y) -> V x, (V y, P y) -> P x) -> V x, (V y, P y) -> P x
thm 361 : V (P : a -> Prop), (-(V y, P y) -> V x, (V y, P y) -> P x) ->
  V x, (V y, P y) -> P x := 354 353

thm 367 : (-T) = F := not_def \f, f T = F -> (-T) = F
thm 368 : (-T) = F -> V P, P (-T) -> P F := eq_def \f, f (-T) F
thm not_T_rw : V P, P (-T) -> P F := 368 367
pragma add_simp not_T_rw

thm 383 : V P, P = (--P) := prop_ext \x, x = (--x)
thm 384 : V f, (V P, P = f P) -> (\P, P) = f := fn_ext \P, P
thm 385 : (V P, P = (--P)) -> (\P, P) = (\P, --P) :=
  384 (\P, --P)
thm 386 : (\P, P) = (\P, --P) := 385 383
thm 387 : (\P, P) = (\P, --P) -> V Q, Q (\P, P) -> Q (\P, --P) :=
  eq_def \f, f (\P, P) (\P, --P)
thm not_not_rw' : V Q, Q (\P, P) -> Q (\P, --P) := 387 386

thm eq_refl : V x, x = x := eq_def
  \f, (V (x : a), f x x) -> V (x : a), x = x

thm 400 : (\P Q, -P -> Q (--P)) = (\P Q, -P -> Q F) ->
  (\P Q, -P -> Q P) = (\P Q, -P -> Q F) := not_not_rw' \f,
  (\P Q, -P -> Q (f P)) = (\P Q, -P -> Q F) ->
  (\P Q, -P -> Q P) = (\P Q, -P -> Q F)
thm 401 : ((\P Q, -P -> Q (--P)) = (\P Q, -P -> Q F) ->
  (\P Q, -P -> Q P) = (\P Q, -P -> Q F)) ->
  (\P Q, -P -> Q F) = (\P Q, -P -> Q F) ->
  (\P Q, -P -> Q P) = (\P Q, -P -> Q F) := imp_pos_rw \f,
  (\P Q, f (-P) # \z, Q (-z)) = (\P Q, -P -> Q F) ->
  (\P Q, -P -> Q P) = (\P Q, -P -> Q F)
thm 404 : (\P Q, -P -> Q F) = (\P Q, -P -> Q F) ->
  (\P Q, -P -> Q P) = (\P Q, -P -> Q F) := 401 400
thm 405 : (\P Q, -P -> Q F) = (\P Q, -P -> Q F) :=
  eq_refl \P Q, -P -> Q F
thm 406 : (\P Q, -P -> Q P) = (\P Q, -P -> Q F) :=
  404 405
thm 407 : (\P Q, -P -> Q P) = (\P Q, -P -> Q F) ->
  V R, R (\P Q, -P -> Q P) -> R (\P Q, -P -> Q F) :=
  eq_def \f, f (\P Q, -P -> Q P) (\P Q, -P -> Q F)
thm imp_neg_rw : V R, R (\P Q, -P -> Q P) ->
  R (\P Q, -P -> Q F) := 407 406

thm 408 : (V (P : a -> Prop), (-(V y, P y) ->
  V x, (V y, P y) -> P x) -> V x, (V y, P y) -> P x) ->
  V (P : a -> Prop) x, (V y, P y) -> P x := imp_neg_rw
  \f, V (P : a -> Prop), (f (V y, P y) # \z, V x, z -> P x) ->
  V x, (V y, P y) -> P x
thm of_univ : V P x, (V y, P y) -> P x := 408 361

To remove a simplification rule, the syntax pragma remove_simp <theorem name> can be used. For example:

pragma remove_simp 503
pragma remove_simp 418
pragma remove_simp 423
pragma remove_simp 284

Technical rewriting theorems

def IMP := \P Q, P -> Q

thm IMP_pos_rw_1 : (V R, R (\P Q, P -> Q P) -> R (\P Q, P -> Q T)) ->
  V R, R (\P Q, IMP P # Q P) -> R (\P Q, P -> Q T) :=
  IMP_def \f, ((V R, R (\P Q, P -> Q P) -> R (\P Q, P -> Q T)) ->
  V R, R (\P Q, f P # Q P) -> R (\P Q, P -> Q T)) ->
  (V R, R (\P Q, P -> Q P) -> R (\P Q, P -> Q T)) ->
  V R, R (\P Q, IMP P # Q P) -> R (\P Q, P -> Q T)
thm IMP_pos_rw : V R, R (\P Q, IMP P # Q P) -> R (\P Q, P -> Q T) :=
  IMP_pos_rw_1 imp_pos_rw
pragma add_simp IMP_pos_rw

thm IMP_neg_rw_1 : (V R, R (\P Q, -P -> Q P) -> R (\P Q, -P -> Q F)) ->
  V R, R (\P Q, IMP (-P) # Q P) -> R (\P Q, -P -> Q F) :=
  IMP_def \f, ((V R, R (\P Q, -P -> Q P) -> R (\P Q, -P -> Q F)) ->
  V R, R (\P Q, f (-P) # Q P) -> R (\P Q, -P -> Q F)) ->
  (V R, R (\P Q, -P -> Q P) -> R (\P Q, -P -> Q F)) ->
  V R, R (\P Q, IMP (-P) # Q P) -> R (\P Q, -P -> Q F)
thm IMP_neg_rw : V R, R (\P Q, IMP (-P) # Q P) -> R (\P Q, -P -> Q F) :=
  IMP_neg_rw_1 imp_neg_rw
pragma add_simp IMP_neg_rw

;-----

thm eq_T_rw : V Q, Q (\P, P = T) -> Q (\P, P) :=
  eq_T_rw' \f, V Q, Q (\P, f P) -> Q (\P, P)
pragma add_simp eq_T_rw

thm not_not_rw : V Q, Q (\P, --P) -> Q (\P, P) :=
  not_not_rw' \f, V Q, Q (\P, f P) -> Q (\P, P)
pragma add_simp not_not_rw

thm eq_refl_rw : V P, P (\x, x = x) -> P (\x, T) :=
  eq_def \f, (V P, P (\x, f x x) -> P (\x, T)) ->
  V P, P (\x, x = x) -> P (\x, T)
pragma remove_simp prop_eq_refl_rw
pragma add_simp eq_refl_rw

thm imp_F_rw : V P, P (\Q, Q -> F) -> P (\Q, -Q) :=
  not_def \f, (V P, P (\Q, Q -> F) -> P (\Q, f Q)) ->
  V P, P (\Q, Q -> F) -> P (\Q, -Q)
pragma add_simp imp_F_rw

thm 510 : V Q, (\P, -(V x, P x) -> Q) = (\P, V x, -P x -> Q) :=
  prop_ext \z, (\P, -(V x, P x) -> z) = (\P, V x, -P x -> z)
thm 511 : V f, (V Q, (\P, -(V x, P x) -> Q) = f Q) -> (\Q P, -(V x, P x) -> Q) = f :=
  fn_ext \Q P, -(V x, P x) -> Q
thm 512 : (V Q, (\P, -(V (x : a), P x) -> Q) = (\P, V x, -P x -> Q)) ->
  (\Q P, -(V (x : a), P x) -> Q) = (\Q P, V x, -P x -> Q) := 511 \Q P, V x, -P x -> Q
thm 513 : (\Q P, -(V (x : a), P x) -> Q) = (\Q P, V x, -P x -> Q) := 512 510
thm 514 : (\Q P, -(V (x : a), P x) -> Q) = (\Q P, V x, -P x -> Q) ->
  V R, R (\Q P, -(V (x : a), P x) -> Q) -> R (\Q P, V x, -P x -> Q) :=
  eq_def \f, f (\Q P, -(V (x : a), P x) -> Q) (\Q P, V x, -P x -> Q)
thm not_univ_imp_rw : V R, R (\Q P, -(V x, P x) -> Q) ->
  R (\Q P, V x, -P x -> Q) := 514 513
pragma add_simp not_univ_imp_rw

;-----

thm rw_T_of : V P, P -> V R, R P -> R T :=
  IMP_def \f, V P, f P # V R, R P -> R T

;-----

thm 515 : V P, (\Q, -P -> -Q) = (\Q, Q -> P) :=
  prop_ext \z, (\Q, -z -> -Q) = (\Q, Q -> z)
thm 516 : V f, (V P, (\Q, -P -> -Q) = f P) -> (\P Q, -P -> -Q) = f :=
  fn_ext \P Q, -P -> -Q
thm 517 : (V P, (\Q, -P -> -Q) = (\Q, Q -> P)) -> (\P Q, -P -> -Q) = (\P Q, Q -> P) :=
  516 \P Q, Q -> P
thm 518 : (\P Q, -P -> -Q) = (\P Q, Q -> P) := 517 515
thm 519 : (\P Q, -P -> -Q) = (\P Q, Q -> P) ->
  V R, R (\P Q, -P -> -Q) -> R (\P Q, Q -> P) :=
  eq_def \f, f (\P Q, -P -> -Q) (\P Q, Q -> P)
thm not_imp_not_rw : V R, R (\P Q, -P -> -Q) -> R (\P Q, Q -> P) := 519 518

thm 520 : (V P x, P x -> P (TAU (x : a), P x)) ->
  V P, -P (TAU (x : a), P x) -> V x, -P x :=
  not_imp_not_rw \f, V P, f (V x, -P x) (-P (TAU x, P x))
thm 521 : V P, -P (TAU x, P x) -> V x, -P x := 520 tau_spec
thm 522 : V f, (V P, (-P (TAU x, P x) -> V x, -P x) = f P) ->
  (\P, -P (TAU x, P x) -> V x, -P x) = f :=
  fn_ext \P, -P (TAU x, P x) -> V x, -P x
thm 523 : (V P, (-P (TAU (x : a), P x) -> V x, -P x)) ->
  (\P, -P (TAU (x : a), P x) -> V x, -P x) = (\x, T) := 522 \P, T
thm 524 : (\P, -P (TAU (x : a), P x) -> V x, -P x) = (\x, T) := 523 521
thm 525 : (\P, -P (TAU (x : a), P x) -> V x, -P x) = (\x, T) ->
  V Q, Q (\P, -P (TAU (x : a), P x) -> V x, -P x) -> Q (\x, T) :=
  eq_def \f, f (\P, -P (TAU (x : a), P x) -> V x, -P x) (\x, T)
thm 526 : V Q, Q (\P, -P (TAU (x : a), P x) -> V x, -P x) -> Q (\x, T) :=
  525 524
thm univ_of_tau : V P, P (TAU x, -P x) -> V x, P x :=
  526 \f, (V P, f # \x, -P x) ->
  V P, P (TAU x, -P x) -> V x, P x

;-----

def P2' := \P, (V x, P x) = (P = (\x, T))
def P2 := TAU P, -P2' P

thm 527 : V f, (V (x : a), P2 x = f x) -> P2 = f := fn_ext P2
thm 528 : (V (x : a), P2 x) -> P2 = (\(x : a), T) := 527 \x, T
thm 529 : V Q, (V Q, Q P2 -> Q (\(x : a), T)) -> Q P2 -> Q (\(x : a), T) :=
  of_univ \Q, Q P2 -> Q (\(x : a), T)
thm 530 : (V Q, Q P2 -> Q (\(x : a), T)) -> V (x : a), P2 x :=
  529 \P, V x, P x -> P2 x
thm 531 : ((V Q, Q P2 -> Q (\(x : a), T)) -> V (x : a), P2 x) ->
  P2 = (\(x : a), T) -> V (x : a), P2 x := eq_def \f,
  (f P2 (\(x : a), T) -> V (x : a), P2 x) ->
  P2 = (\(x : a), T) -> V (x : a), P2 x
thm 532 : P2 = (\(x : a), T) -> V (x : a), P2 x := 531 530
thm 533 : V Q, ((V (x : a), P2 x) -> Q) -> (Q -> (V (x : a), P2 x)) ->
  (V (x : a), P2 x) = Q := eq_of_imp_imp V (x : a), P2 x
thm 534 : ((V (x : a), P2 x) -> P2 = (\(x : b), T)) ->
  (P2 = (\(x : b), T) -> (V (x : a), P2 x)) ->
  (V (x : a), P2 x) = (P2 = (\(x : b), T)) :=
  533 P2 = \(x : b), T
thm 535 : (P2 = (\(x : a), T) -> (V (x : a), P2 x)) ->
  (V (x : a), P2 x) = (P2 = (\(x : a), T)) := 534 528
thm 536 : (V (x : a), P2 x) = (P2 = (\(x : a), T)) := 535 532
thm 537 : P2' (TAU (P : a -> Prop), -P2' P) -> V (P : a -> Prop), P2' P :=
  univ_of_tau P2'
thm 538 : (P2' (TAU (P : a -> Prop), -P2' P) -> V (P : a -> Prop), P2' P) ->
  P2' (\(x : a), P2 x) -> V (P : a -> Prop), P2' P := P2_def \f,
  (P2' (\(x : a), f x) -> V (P : a -> Prop), P2' P) ->
  P2' (\(x : a), P2 x) -> V (P : a -> Prop), P2' P
thm 539 : P2' (\(x : a), P2 x) -> V (P : a -> Prop), P2' P := 538 537
thm 540 : (P2' (\(x : a), P2 x) -> V (P : a -> Prop), P2' P) ->
  (V (x : a), P2 x) = (P2 = (\(x : a), T)) ->
  V P, (V (x : a), P x) = (P = (\(x : a), T)) :=
  P2'_def \P2', P2' (\(x : a), P2 x) -> V (P : a -> Prop), P2' P
thm 541 : (V (x : a), P2 x) = (P2 = (\(x : a), T)) ->
  V P, (V (x : a), P x) = (P = (\(x : a), T)) := 540 539
thm 542 : V P, (V (x : a), P x) = (P = (\(x : a), T)) := 541 536
thm 543 : V f, (V P, (V (x : a), P x) = f P) -> (\P, V (x : a), P x) = f :=
  fn_ext \P, V (x : a), P x
thm 544 : (V P, (V (x : a), P x) = (P = \(x : a), T)) ->
  (\P, V (x : a), P x) = (\P, P = \(x : a), T) :=
  543 \P, P = \(x : a), T
thm 545 : (\P, V (x : a), P x) = (\P, P = \(x : a), T) := 544 542
thm 546 : (\P, V (x : a), P x) = (\P, P = \(x : a), T) ->
  V Q, Q (\P, V (x : a), P x) -> Q (\P, P = \(x : a), T) :=
  eq_def \f, f (\P, V (x : a), P x) (\P, P = \(x : a), T)
thm univ_rw_eq_T : V Q, Q (\P, V (x : a), P x) -> Q (\P, P = \(x : a), T) :=
  546 545

;-----

thm rw_F_not : V P, -P -> V Q, Q P -> Q F :=
  prop_ext \P, -P -> V Q, Q P -> Q F

pragma remove_simp not_univ_imp_rw
thm 563 : V P, (V Q, Q T -> Q F) -> P T -> P F :=
  of_univ \Q, Q T -> Q F
thm 564 : -(V Q, Q T -> Q F) := 563 \x, x
thm 565 : -(V Q, Q T -> Q F) -> -(T = F) := eq_def \f,
  (-(V Q, Q T -> Q F) -> -(f T F)) -> -(V Q, Q T -> Q F) -> -(T = F)
thm 566 : -(T = F) := 565 564
thm 567 : -(T = F) -> V P, P (T = F) -> P F := rw_F_not T = F
thm 568 : V P, P (T = F) -> P F := 567 566
pragma add_simp not_univ_imp_rw

thm 562 : (T = F) = F -> V P, (T = P) = P := prop_ext \P, (T = P) = P
thm 569 : (T = F) = F := 568 \x, x = F -> (T = F) = F
thm 570 : V P, (T = P) = P := 562 569
thm 571 : V f, (V P, (T = P) = f P) -> (\P, T = P) = f := fn_ext \P, T = P
thm 572 : (V P, (T = P) = P) -> (\P, T = P) = (\P, P) := 571 \P, P
thm 573 : (\P, T = P) = (\P, P) := 572 570
thm 574 : (\P, T = P) = (\P, P) -> V Q, Q (\P, T = P) -> Q (\P, P) :=
  eq_def \f, f (\P, T = P) (\P, P)
thm T_eq_rw : V Q, Q (\P, T = P) -> Q (\P, P) := 574 573
pragma add_simp T_eq_rw

thm 575 : V P, (F = P) = (-P) := prop_ext \P, (F = P) = (-P)
thm 576 : V f, (V P, (F = P) = f P) -> (\P, F = P) = f := fn_ext \P, F = P
thm 577 : (V P, (F = P) = (-P)) -> (\P, F = P) = (\P, -P) := 576 \P, -P
thm 578 : (\P, F = P) = (\P, -P) := 577 575
thm 579 : (\P, F = P) = (\P, -P) -> V Q, Q (\P, F = P) -> Q (\P, -P) :=
  eq_def \f, f (\P, F = P) (\P, -P)
thm F_eq_rw : V Q, Q (\P, F = P) -> Q (\P, -P) := 579 578
pragma add_simp F_eq_rw

thm 580 : V P, (-P -> P) = P := prop_ext \P, (-P -> P) = P
thm 581 : V f, (V P, (-P -> P) = f P) -> (\P, -P -> P) = f :=
  fn_ext \P, -P -> P
thm 582 : (V P, (-P -> P) = P) -> (\P, -P -> P) = (\P, P) := 581 \P, P
thm 583 : (\P, -P -> P) = (\P, P) := 582 580
thm 584 : (\P, -P -> P) = (\P, P) -> V Q, Q (\P, -P -> P) -> Q (\P, P) :=
  eq_def \f, f (\P, -P -> P) (\P, P)
thm not_imp_this_rw : V Q, Q (\P, -P -> P) -> Q (\P, P) := 584 583
pragma add_simp not_imp_this_rw

thm 561 : V P, (\Q, P = Q -> P) = (\Q, P = Q -> Q) :=
  prop_ext \P, (\Q, P = Q -> P) = (\Q, P = Q -> Q)
thm 585 : V f, (V P, (\Q, P = Q -> P) = f P) -> (\P Q, P = Q -> P) = f :=
  fn_ext \P Q, P = Q -> P
thm 586 : (V P, (\Q, P = Q -> P) = (\Q, P = Q -> Q)) ->
  (\P Q, P = Q -> P) = (\P Q, P = Q -> Q) := 585 \P Q, P = Q -> Q
thm 587 : (\P Q, P = Q -> P) = (\P Q, P = Q -> Q) := 586 561
thm 588 : (\P Q, P = Q -> P) = (\P Q, P = Q -> Q) ->
  V R, R (\P Q, P = Q -> P) -> R (\P Q, P = Q -> Q) :=
  eq_def \f, f (\P Q, P = Q -> P) (\P Q, P = Q -> Q)
thm eq_imp_this_rw : V R, R (\P Q, P = Q -> P) -> R (\P Q, P = Q -> Q) :=
  588 587

;-----

thm 614 : (V P (x : a), (V y, P y) -> P x) ->
  V P, (\(x : a), (V y, P y) -> P x) = (\x, T) :=
  univ_rw_eq_T \f, V P, f # \(x : a), (V y, P y) -> P x
thm 615 : V P, (\(x : a), (V y, P y) -> P x) = (\x, T) := 614 of_univ
thm 616 : V f, (V P, (\(x : a), (V y, P y) -> P x) = f P) ->
  (\P (x : a), (V y, P y) -> P x) = f := fn_ext
  \P (x : a), (V y, P y) -> P x
thm 617 : (V P, (\(x : a), (V y, P y) -> P x) = (\x, T)) ->
  (\P (x : a), (V y, P y) -> P x) = (\P x, T) := 616 \P x, T
thm 618 : (\P (x : a), (V y, P y) -> P x) = (\P x, T) := 617 615
thm 619 : (\P (x : a), (V y, P y) -> P x) = (\P x, T) ->
  V Q, Q (\P (x : a), (V y, P y) -> P x) -> Q (\P x, T) :=
  eq_def \f, f (\P (x : a), (V y, P y) -> P x) (\P x, T)
thm of_univ_rw : V Q, Q (\P x, (V y, P y) -> P x) -> Q (\P x, T) :=
  619 618

thm 620 : (V Q, Q (\P (x y : a), (V z, P z) -> P x) -> Q (\P x y, T)) ->
  V Q, Q (\P (x y : a), (V z, P z) -> P x) ->
  Q (\P (x y : a), (V z, P z) -> P y) := of_univ_rw \f,
  (V Q, Q (\P (x y : a), (V z, P z) -> P x) -> Q (\P x y, f P y)) ->
  V Q, Q (\P (x y : a), (V z, P z) -> P x) ->
  Q (\P (x y : a), (V z, P z) -> P y)
thm 621 : V Q, Q (\P (x y : a), (V z, P z) -> P x) -> Q (\P x y, T) :=
  of_univ_rw \f, (V Q, Q (\P (x y : a), f P x) -> Q (\P x y, T)) ->
  V Q, Q (\P (x y : a), (V z, P z) -> P x) -> Q (\P x y, T)
thm of_univ_rw' : V Q, Q (\P x y, (V z, P z) -> P x) ->
  Q (\P x y, (V z, P z) -> P y) := 620 621

thm 622 : V P, (\Q R, (P -> Q) -> P -> R) = (\Q R, P -> Q -> R) :=
  prop_ext \P, (\Q R, (P -> Q) -> P -> R) = (\Q R, P -> Q -> R)
thm 623 : V f, (V P, (\Q R, (P -> Q) -> P -> R) = f P) ->
  (\P Q R, (P -> Q) -> P -> R) = f := fn_ext \P Q R, (P -> Q) -> P -> R
thm 624 : (V P, (\Q R, (P -> Q) -> P -> R) = (\Q R, P -> Q -> R)) ->
  (\P Q R, (P -> Q) -> P -> R) = (\P Q R, P -> Q -> R) :=
  623 \P Q R, P -> Q -> R
thm 625 : (\P Q R, (P -> Q) -> P -> R) = (\P Q R, P -> Q -> R) := 624 622
thm 626 : (\P Q R, (P -> Q) -> P -> R) = (\P Q R, P -> Q -> R) ->
  V S, S (\P Q R, (P -> Q) -> P -> R) -> S (\P Q R, P -> Q -> R) :=
  eq_def \f, f (\P Q R, (P -> Q) -> P -> R) (\P Q R, P -> Q -> R)
thm ax_s_rw : V S, S (\P Q R, (P -> Q) -> P -> R) -> S (\P Q R, P -> Q -> R) :=
  626 625

thm imp_same_imp_rw : V R, R (\P Q, P -> P -> Q) -> R (\P Q, P -> Q) :=
  imp_pos_rw \f, V R, R (\P Q, P -> P -> Q) -> R (\P Q, f P (\z, z -> Q))
pragma add_simp imp_same_imp_rw

thm 628 : (V Q, Q (\(x y : a) P, (V R, R x -> R y) -> P x -> P y) ->
  Q (\x y P, T)) -> V Q, Q (\(x y : a) P, x = y -> P x -> P y) ->
  Q (\x y P, T) := eq_def \f, (V Q, Q (\(x y : a) P, f x y ->
  P x -> P y) -> Q (\x y P, T)) -> V Q, Q (\(x y : a) P, x = y -> P x -> P y) ->
  Q (\x y P, T)
thm 629 : V Q, Q (\(x y : a) P, (V R, R x -> R y) -> P x -> P y) ->
  Q (\x y P, T) := of_univ_rw \f, (V Q, Q (\(x y : a) P,
  f (\R, R x -> R y) P) -> Q (\x y P, T)) -> V Q, Q (\(x y : a) P,
  (V R, R x -> R y) -> P x -> P y) -> Q (\x y P, T)
thm apply_imp_of_eq_rw : V Q, Q (\(x y : a) P, x = y -> P x -> P y) ->
  Q (\x y P, T) := 628 629
thm apply_imp_of_eq_rw' : V Q, Q (\(x y : a) P, x = y -> P y -> P x) ->
  Q (\x y P, T) := apply_imp_of_eq_rw \f,
  (V Q, Q (\(x y : a) P, f x y # \z, P z -> P x) -> Q (\x y P, T)) ->
  V Q, Q (\(x y : a) P, x = y -> P y -> P x) -> Q (\x y P, T)

thm 634 : V P, P (\(x y : a), x = y -> y = x) -> P (\x y, T) :=
  apply_imp_of_eq_rw \f,
  (V P, P (\(x y : a), f x y # \z, z = x) -> P (\x y, T)) ->
  V P, P (\(x y : a), x = y -> y = x) -> P (\x y, T)

;-----

thm 635 : (V Q, Q (\(x y : a) P, x = y -> (x = y -> P x = P y) -> P x) ->
  Q (\x y P, x = y -> (x = y -> P x = P y) -> P y)) ->
  V Q, Q (\(x y : a) P, x = y -> P x) -> Q (\x y P, x = y -> P y) :=
  apply_imp_of_eq_rw \f,
  (V Q, Q (\(x y : a) P, x = y -> (x = y -> P x = P y) -> P x) ->
  Q (\x y P, x = y -> (x = y -> P x = P y) -> P y)) ->
  V Q, Q (\(x y : a) P, x = y -> (f x y # \z, P x = P z) -> P x) ->
  Q (\x y P, x = y -> (f x y # \z, P x = P z) -> P y)
thm 636 : (V Q, Q (\(x y : a) P, x = y -> P x = P y -> P x) ->
  Q (\x y P, x = y -> P x = P y -> P y)) ->
  V Q, Q (\(x y : a) P, x = y -> (x = y -> P x = P y) -> P x) ->
  Q (\x y P, x = y -> (x = y -> P x = P y) -> P y) :=
  imp_pos_rw \f,
  (V Q, Q (\(x y : a) P, f (x = y) # \z, (z -> P x = P y) -> P x) ->
  Q (\x y P, f (x = y) # \z, (z -> P x = P y) -> P y)) ->
  V Q, Q (\(x y : a) P, x = y -> (x = y -> P x = P y) -> P x) ->
  Q (\x y P, x = y -> (x = y -> P x = P y) -> P y)
thm 637 : V Q, Q (\(x y : a) P, x = y -> P x = P y -> P x) ->
  Q (\x y P, x = y -> P x = P y -> P y) := eq_imp_this_rw \f,
  (V Q, Q (\(x y : a) P, x = y -> f (P x) (P y)) ->
  Q (\x y P, x = y -> P x = P y -> P y)) ->
  V Q, Q (\(x y : a) P, x = y -> P x = P y -> P x) ->
  Q (\x y P, x = y -> P x = P y -> P y)
thm 638 : V Q, Q (\(x y : a) P, x = y -> (x = y -> P x = P y) -> P x) ->
  Q (\x y P, x = y -> (x = y -> P x = P y) -> P y) := 636 637
thm eq_imp_rw : V Q, Q (\x y P, x = y -> P x) -> Q (\x y P, x = y -> P y) :=
  635 638

thm 557 : (V R, R (\(x y : a) P, x = y -> P x) -> R (\x y P, x = y -> P y)) ->
  V Q, Q (\(x y : a) P, (V Q, Q x -> Q y) -> P x) ->
  Q (\x y P, (V Q, Q x -> Q y) -> P y) := eq_def \f,
  V R, R (\x y P, f x y -> P x) -> R (\x y P, f x y -> P y)
thm rw_imp_rw : V Q, Q (\x y P, (V Q, Q x -> Q y) -> P x) ->
  Q (\x y P, (V Q, Q x -> Q y) -> P y) := 557 eq_imp_rw

;-----

def UNIT := TAU (x : Prop), T
def NIL := UNIT
def CONS := \x y, UNIT
def UNF := \x, x
def PROOF := \(x : Prop), x
def PROOF' := \(x : Prop), T
def RW := \(S P : Prop), P
def RW_1 := \(S P : Prop), P
def RW_2 := \(S P Q : Prop), P -> Q
def RW_3 := \(P : a -> Prop) (S P Q : Prop), P -> Q

thm UNF_of : V x y, (V P, P x -> P y) -> V P, P (UNF x) -> P y :=
  UNF_def \f, V x y, (V P, P (f x) -> P y) -> V P, P (UNF x) -> P y

thm PROOF_of_1 : (V S, IMP (UNF S) # V P, P S -> P T) ->
  V S, IMP (UNF S) # V P, P (PROOF S) -> P T :=
  PROOF_def \f, (V S, IMP (UNF S) # V P, P (f S) -> P T) ->
  V S, IMP (UNF S) # V P, P (PROOF S) -> P T
thm PROOF_of_2 : ((V S, IMP (UNF S) # V P, P S -> P T) ->
  V S, IMP (UNF S) # V P, P (PROOF S) -> P T) ->
  V S, IMP (UNF S) # V P, P (PROOF S) -> P T := UNF_def \f,
  ((V S, IMP (UNF S) # V P, P S -> P T) -> V S, IMP (UNF S) # V P, P (PROOF S) -> P T) ->
  (V S, IMP (f S) # V P, P S -> P T) -> V S, IMP (UNF S) # V P, P (PROOF S) -> P T
thm PROOF_of_3 : V S, IMP (UNF S) # V P, P (PROOF S) -> P T := PROOF_of_2 PROOF_of_1
thm PROOF_of_4 : (V S, IMP (UNF S) # V P, P (PROOF S) -> P T) ->
  V S, UNF S -> V P, P (PROOF S) -> P T :=
  IMP_def \f, V S, f (UNF S) # V P, P (PROOF S) -> P T
thm PROOF_of : V S, UNF S -> V P, P (PROOF S) -> P T :=
  PROOF_of_4 PROOF_of_3

thm 590 : (V S, S -> V P, P (PROOF' S) -> P S) ->
  V S, UNF S -> V P, P (PROOF' S) -> P S :=
  UNF_def \f, (V S, f S -> V P, P (PROOF' S) -> P S) ->
  V S, UNF S -> V P, P (PROOF' S) -> P S
thm 591 : (V S, S -> V P, P T -> P S) -> V S, S ->
  V P, P (PROOF' S) -> P S := PROOF'_def \f,
  (V S, S -> V P, P (f S) -> P S) -> V S, S -> V P, P (PROOF' S) -> P S
thm 592 : V S, S -> V P, P T -> P S :=
  IMP_def \f, V S, f S # V P, P T -> P S
thm 593 : V S, S -> V P, P (PROOF' S) -> P S := 591 592
thm PROOF'_of : V S, UNF S -> V P, P (PROOF' S) -> P S := 590 593

thm PROOF_T_rw : V P, P (PROOF T) -> P T :=
  PROOF_def \f, (V P, P (f T) -> P T) -> V P, P (PROOF T) -> P T
pragma add_simp PROOF_T_rw

thm PROOF'_T_rw : V P, P (PROOF' T) -> P T :=
  PROOF'_def \f, (V P, P (f T) -> P T) -> V P, P (PROOF' T) -> P T
pragma add_simp PROOF'_T_rw

thm RW_NIL : V P, P (\Q, RW NIL Q) -> P (\Q, Q) :=
  RW_def \f, V P, P (\Q, RW NIL Q) -> P (\Q, f NIL Q)
pragma add_simp RW_NIL

thm RW_CONS_1 : V P, P (\(Q R S : Prop), RW (CONS Q R) S) -> P (\Q R S, RW R S) :=
  RW_def \f, (V P, P (\(Q R S : Prop), f (CONS Q R) S) -> P (\Q R S, f R S)) ->
  V P, P (\Q R S, RW (CONS Q R) S) -> P (\Q R S, RW R S)
thm RW_CONS_2 : (V P, P (\(Q R S : Prop), RW (CONS Q R) S) -> P (\Q R S, RW R S)) ->
  V P, P (\(Q R S : Prop), RW (CONS Q R) S) -> P (\Q R S, RW R (RW_1 Q S)) :=
  RW_1_def \f, (V P, P (\(Q R S : Prop), RW (CONS Q R) S) -> P (\Q R S, RW R (f Q S))) ->
  V P, P (\(Q R S : Prop), RW (CONS Q R) S) -> P (\Q R S, RW R (RW_1 Q S))
thm RW_CONS' : V P, P (\(Q R S : Prop), RW (CONS Q R) S) -> P (\Q R S, RW R (RW_1 Q S)) :=
  RW_CONS_2 RW_CONS_1

thm 594 : (V P, P (\S Q, Q) -> P (\S Q, RW_2 S (PROOF' S) Q)) ->
  V P, P (\S Q, RW_1 S Q) -> P (\S Q, RW_2 S (PROOF' S) Q) :=
  RW_1_def \f, (V P, P (\S Q, f S Q) -> P (\S Q, RW_2 S (PROOF' S) Q)) ->
  V P, P (\S Q, RW_1 S Q) -> P (\S Q, RW_2 S (PROOF' S) Q)
thm 595 : (V P, P (\S Q, Q) -> P (\S Q, PROOF' S -> Q)) ->
  V P, P (\S Q, Q) -> P (\S Q, RW_2 S (PROOF' S) Q) :=
  RW_2_def \f, (V P, P (\S Q, Q) -> P (\S Q, f S (PROOF' S) Q)) ->
  V P, P (\S Q, Q) -> P (\S Q, RW_2 S (PROOF' S) Q)
thm 596 : V P, P (\S Q, Q) -> P (\S Q, PROOF' S -> Q) :=
  PROOF'_def \f, (V P, P (\S Q, Q) -> P (\S Q, f S -> Q)) ->
  V P, P (\S Q, Q) -> P (\S Q, PROOF' S -> Q)
thm 597 : V P, P (\S Q, Q) -> P (\S Q, RW_2 S (PROOF' S) Q) := 595 596
thm RW_1_rw : V P, P (\S Q, RW_1 S Q) -> P (\S Q, RW_2 S (PROOF' S) Q) := 594 597

thm 700 : (V P, P (\(Q R S : Prop), RW (CONS Q R) S) -> P (\Q R S, RW R (RW_1 Q S))) ->
  V P, P (\(Q R S : Prop), RW (CONS Q R) S) -> P (\Q R S, RW R # RW_2 Q (PROOF' Q) S) :=
  RW_1_rw \f, (V P, P (\(Q R S : Prop), RW (CONS Q R) S) -> P (\Q R S, RW R (RW_1 Q S))) ->
  V P, P (\(Q R S : Prop), RW (CONS Q R) S) -> P (\Q R S, RW R # f Q S)
thm RW_CONS : V P, P (\(Q R S : Prop), RW (CONS Q R) S) ->
  P (\Q R S, RW R # RW_2 Q (PROOF' Q) S) := 700 RW_CONS'
pragma add_simp RW_CONS

thm 605 : (V P, P (\(S : Prop) (x y : a) Q, (V R, R x -> R y) -> Q x) ->
  P (\(S : Prop) (x y : a) Q, (PROOF' S -> V R, R x -> R y) -> Q y)) ->
  V P, P (\(S : Prop) (x y : a) Q, RW_2 S (V R, R x -> R y) (Q x)) ->
  P (\(S : Prop) (x y : a) Q, (PROOF' S -> V R, R x -> R y) -> Q y) :=
  RW_2_def \f,
  (V P, P (\(S : Prop) (x y : a) Q, f S (V R, R x -> R y) (Q x)) ->
  P (\(S : Prop) (x y : a) Q, (PROOF' S -> V R, R x -> R y) -> Q y)) ->
  V P, P (\(S : Prop) (x y : a) Q, RW_2 S (V R, R x -> R y) (Q x)) ->
  P (\(S : Prop) (x y : a) Q, (PROOF' S -> V R, R x -> R y) -> Q y)
thm 606 : (V P, P (\(S : Prop) (x y : a) Q, (V R, R x -> R y) -> Q x) ->
  P (\(S : Prop) (x y : a) Q, (V R, R x -> R y) -> Q y)) ->
  V P, P (\(S : Prop) (x y : a) Q, (V R, R x -> R y) -> Q x) ->
  P (\(S : Prop) (x y : a) Q, (PROOF' S -> V R, R x -> R y) -> Q y) :=
  PROOF'_def \f,
  (V P, P (\(S : Prop) (x y : a) Q, (V R, R x -> R y) -> Q x) ->
  P (\(S : Prop) (x y : a) Q, (f S -> V R, R x -> R y) -> Q y)) ->
  V P, P (\(S : Prop) (x y : a) Q, (V R, R x -> R y) -> Q x) ->
  P (\(S : Prop) (x y : a) Q, (PROOF' S -> V R, R x -> R y) -> Q y)
thm 607 : V P, P (\(S : Prop) (x y : a) Q, (V R, R x -> R y) -> Q x) ->
  P (\(S : Prop) (x y : a) Q, (V R, R x -> R y) -> Q y) := rw_imp_rw \f,
  V P, P (\(S : Prop) (x y : a) Q, (V R, R x -> R y) -> Q x) ->
  P (\(S : Prop) (x y : a) Q, f x y Q)
thm 608 : V P, P (\(S : Prop) (x y : a) Q, (V R, R x -> R y) -> Q x) ->
  P (\(S : Prop) (x y : a) Q, (PROOF' S -> V R, R x -> R y) -> Q y) := 606 607
thm RW_2_rw : V P, P (\(S : Prop) (x y : a) Q, RW_2 S (V R, R x -> R y) (Q x)) ->
  P (\(S : Prop) (x y : a) Q, (PROOF' S -> V R, R x -> R y) -> Q y) := 605 608
pragma add_simp RW_2_rw

thm PROOF_rw_of : V P, P -> V Q, Q (PROOF P) -> Q T :=
  imp_pos_rw \f, (V P, f P # \P, V Q, Q (PROOF P) -> Q T) ->
  V P, P -> V Q, Q (PROOF P) -> Q T

;-----

def BY := \(x : Prop), T
def BY_1 := \(P S : Prop), P = S

thm 609 : (V P, P (\(S xs : Prop), T) -> P (\(S xs : Prop), BY_1 S # RW xs S)) ->
  V P, P (\(S xs : Prop), BY # CONS S xs) -> P (\(S xs : Prop), BY_1 S # RW xs S) :=
  BY_def \f, (V P, P (\(S xs : Prop), f # CONS S xs) ->
  P (\(S xs : Prop), BY_1 S # RW xs S)) -> V P, P (\(S xs : Prop),
  BY # CONS S xs) -> P (\(S xs : Prop), BY_1 S # RW xs S)
thm 610 : (V P, P (\(S xs : Prop), T) -> P (\(S xs : Prop), BY_1 S S)) ->
  V P, P (\(S xs : Prop), T) -> P (\(S xs : Prop), BY_1 S # RW xs S) :=
  RW_def \f, (V P, P (\(S xs : Prop), T) -> P (\(S xs : Prop),
  BY_1 S # f xs S)) -> V P, P (\(S xs : Prop), T) -> P (\(S xs : Prop),
  BY_1 S # RW xs S)
thm 611 : V P, P (\(S xs : Prop), T) -> P (\(S xs : Prop), BY_1 S S) :=
  BY_1_def \f, (V P, P (\(S xs : Prop), T) -> P (\(S xs : Prop), f S S)) ->
  V P, P (\(S xs : Prop), T) -> P (\(S xs : Prop), BY_1 S S)
thm 612 : V P, P (\(S xs : Prop), T) -> P (\(S xs : Prop), BY_1 S # RW xs S) := 610 611
thm BY_CONS : V P, P (\(S xs : Prop), BY # CONS S xs) ->
  P (\(S xs : Prop), BY_1 S # RW xs S) := 609 612
pragma add_simp BY_CONS

thm BY_1_T : V P, P (\S, BY_1 S T) -> P (\S, S) := BY_1_def \f,
  (V P, P (\S, f S T) -> P (\S, S)) -> V P, P (\S, BY_1 S T) -> P (\S, S)
pragma add_simp BY_1_T

thm by_rw : V xs, BY xs := BY_def \f, (V xs, f xs) -> V xs, BY xs

List syntax

The syntax [x1, x2, ..., xn] is translated to CONS x1 # CONS x2 # ... # CONS xn NIL. There is also pragma utilize_rw_thms that we will not explain here. See the implementation for details. Here are more theorems:

def CONS' := CONS

pragma utilize_rw_thms RW_def RW_2_def RW_3_def PROOF'_def

thm 702 : V P, P (\(P : a -> Prop) (Q R S : Prop), RW (CONS' [Q, P] R) S) ->
  P (\P Q R S, RW R # RW_3 P Q (PROOF' Q) S) := by_rw [
  V P, P (\(P : a -> Prop) (Q R S : Prop), RW (CONS' [Q, P] R) S) ->
    P (\P Q R S, RW R # RW_3 P Q (PROOF' Q) S),
  RW_def, RW_def, RW_3_def, PROOF'_def ]

pragma remove_simp RW_CONS

thm 703 : (V P, P (\(P : a -> Prop) (Q R S : Prop), RW (CONS' [Q, P] R) S) ->
  P (\P Q R S, RW R # RW_3 P Q (PROOF' Q) S)) ->
  V P, P (\(P : a -> Prop) (Q R S : Prop), RW (CONS [Q, P] R) S) ->
  P (\P Q R S, RW R # RW_3 P Q (PROOF' Q) S) := CONS'_def \f,
  V P, P (\(P : a -> Prop) (Q R S : Prop), RW (f [Q, P] R) S) ->
  P (\P Q R S, RW R # RW_3 P Q (PROOF' Q) S)
thm RW_CONS_CONS : V P, P (\(P : a -> Prop) (Q R S : Prop), RW (CONS [Q, P] R) S) ->
  P (\P Q R S, RW R # RW_3 P Q (PROOF' Q) S) := 703 702
pragma add_simp RW_CONS_CONS
pragma add_simp RW_CONS

thm RW_3_rw_RW_2 : V P, P (\P S Q R, RW_3 P S Q R) -> P (\P S Q R, RW_2 S Q R) := by_rw [
  V P, P (\P S Q R, RW_3 P S Q R) -> P (\P S Q R, RW_2 S Q R),
  RW_2_def, RW_3_def,
]
pragma utilize_rw_thms RW_3_rw_RW_2

thm RW_3_rw : V P, P (\(S : Prop) (x y : a) Q, RW_3 Q S (V R, R x -> R y) (Q x)) ->
  P (\(S : Prop) (x y : a) Q, (PROOF' S -> V R, R x -> R y) -> Q y) := by_rw [
  V P, P (\(S : Prop) (x y : a) Q, RW_3 Q S (V R, R x -> R y) (Q x)) ->
    P (\(S : Prop) (x y : a) Q, (PROOF' S -> V R, R x -> R y) -> Q y),
  RW_3_rw_RW_2,
]
pragma add_simp RW_3_rw

;-----

pragma utilize_rw_thms univ_rw_eq_T

thm 701 : V Q, Q (\P f, (V (x : a), P x) -> V x, P (f x)) -> Q (\P f, T) := by_rw [
  V Q, Q (\P f, (V (x : a), P x) -> V x, P (f x)) -> Q (\P f, T),
  [univ_rw_eq_T, \g, V Q, Q (\P f, g P -> V x, P (f x)) -> Q (\P f, T)],
]

External resources

• Interpreter