Rule: baseEquality
This rule proved as lemma rule_base_equality_true3 in file rules/rules_base.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ Base Base ∈ Type

  BY baseEquality ()
  
  No Subgoals

Rule: imageEquality
This rule proved as lemma rule_image_equality_true in file rules/rules_image.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ Image(A1,f1) Image(A2,f2) ∈ Type

  BY imageEquality !parameter{i:l} ()
  
  H  ⊢ f1 f2 ∈ Base
  H  ⊢ A1 A2 ∈ Type

Rule: equalityEqualityBase
This rule proved as lemma rule_equality_equality_base_or_true in file rules/rules_equality.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (a11 a12 ∈ A1) (a21 a22 ∈ A2) ∈ Type

  BY equalityEqualityBase ()
  
  H  ⊢ A1 A2 ∈ Type
  H  ⊢ a11 a21 ∈ Image((x:Unit? × case of inl() => A1 inr() => Base),(λp.(snd(p))))
  H  ⊢ a12 a22 ∈ Image((x:Unit? × case of inl() => A1 inr() => Base),(λp.(snd(p))))

Rule: baseInt
This rule proved as lemma rule_int_subtype_base_true in file rules/rules_squiggle5.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ t1 t2 ∈ Base

  BY baseInt ()
  
  H  ⊢ t1 t2 ∈ ℤ

Rule: baseAtom
This rule proved as lemma rule_atom_subtype_base_true in file rules/rules_squiggle5.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ t1 t2 ∈ Base

  BY baseAtom ()
  
  H  ⊢ t1 t2 ∈ Atom

Rule: sqequalBase
This rule proved as lemma rule_cequiv_base_true in file rules/rules_squiggle.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b

  BY sqequalBase ()
  
  H  ⊢ b ∈ Base

Rule: baseAtomn
This rule proved as lemma rule_uatom_subtype_base_true in file rules/rules_squiggle5.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ Base

  BY baseAtomn !parameter{$n:n}
  
  H  ⊢ b ∈ Atom$n

Rule: atomn_eqEquality
H  ⊢ if a1=$n b1 then s1 else t1 if a2=$n b2 then s2 else t2 ∈ T

  BY atomn_eqEquality v
  
  H  ⊢ a1 a2 ∈ Atom$n
  H  ⊢ b1 b2 ∈ Atom$n
  v:(a1 b1 ∈ Atom$n) ⊢ s1 s2 ∈ T
  v:((a1 b1 ∈ Atom$n) ⟶ Void) ⊢ t1 t2 ∈ T

Rule: freeFromAtomEquality
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ a1#x1:T1 a2#x2:T2 ∈ Type

  BY freeFromAtomEquality ()
  
  H  ⊢ T1 T2 ∈ Type
  H  ⊢ x1 x2 ∈ T1
  H  ⊢ a1 a2 ∈ Atom$n

Rule: isatom1Cases
H  ⊢ ext !((!\\x.isatom1(t;ea;eb)) Ax)

  BY isatom1Cases ()
  
  H  ⊢ 0 ≤ eval in 0
  H  ⊢ t ∈ Base
  x:(t ∈ Atom1) ⊢ ext ea
  x:(∀[u,v:Base].  (isatom1(t;u;v) v)) ⊢ ext eb

Rule: isatom2Cases
H  ⊢ ext !((!\\x.isatom2(t;ea;eb)) Ax)

  BY isatom2Cases ()
  
  H  ⊢ 0 ≤ eval in 0
  H  ⊢ t ∈ Base
  x:(t ∈ Atom2) ⊢ ext ea
  x:(∀[u,v:Base].  (isatom2(t;u;v) v)) ⊢ ext eb

Rule: exceptionNotBottom
This rule proved as lemma rule_exception_not_bottom_true in file rules/rules_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ C

  BY exceptionNotBottom ()
  
  H  ⊢ exception(x; y) ≤ ⊥

Rule: exceptionNotAxiom
This rule proved as lemma rule_exception_not_axiom_true in file rules/rules_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ C

  BY exceptionNotAxiom ()
     
     
  H  ⊢ Ax ≤ exception(x; y)

Rule: isAtom1ReduceTrue
H  ⊢ isatom1(z;a;b) a

  BY isAtom1ReduceTrue ()
  
  H  ⊢ z ∈ Atom1

Rule: callbyvalueAtom
H  ⊢ 0 ≤ eval in 0

  BY callbyvalueAtom ()
  
  H  ⊢ a ∈ Atom

Rule: callbyvalueAtom1
H  ⊢ 0 ≤ eval in 0

  BY callbyvalueAtom1 ()
  
  H  ⊢ a ∈ Atom1

Rule: callbyvalueAtom2
H  ⊢ 0 ≤ eval in 0

  BY callbyvalueAtom2 ()
  
  H  ⊢ a ∈ Atom2

Rule: callbyvalueType
This rule proved as lemma rule_callbyvalue_type_true3 in file rules/rules_uni.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ 0 ≤ eval in 0

  BY callbyvalueType !parameter{i:l}
  
  H  ⊢ T ∈ Type

Rule: applyInt
This rule proved as lemma rule_apply_int_true in file rules/rules_apply_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ≤ ⊥

  BY applyInt ()
  
  H  ⊢ m ∈ ℤ

Rule: isatomCases
H  ⊢ ext !((!\\x.if is an atom then ea otherwise eb) Ax)

  BY isatomCases ()
  
  H  ⊢ 0 ≤ eval in 0
  H  ⊢ t ∈ Base
  x:(t ∈ Atom) ⊢ ext ea
  x:(∀[u,v:Base].  (if is an atom then otherwise v)) ⊢ ext eb

Rule: callbyvalueInt
This rule proved as lemma rule_callbyvalue_int_true3 in file rules/rules_number.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ 0 ≤ eval in 0

  BY callbyvalueInt ()
  
  H  ⊢ a ∈ ℤ

Rule: exceptionMultiply
This rule proved as lemma rule_exception_arith_true3 in file rules/rules_arith_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (exception(u; v)) exception(u; v)

  BY exceptionMultiply ()
  
  H  ⊢ x ∈ ℤ

Rule: exceptionDivide
This rule proved as lemma rule_exception_arith_true3 in file rules/rules_arith_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ x ÷ exception(u; v) exception(u; v)

  BY exceptionDivide ()
  
  H  ⊢ x ∈ ℤ

Rule: exceptionRemainder
This rule proved as lemma rule_exception_arith_true3 in file rules/rules_arith_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ rem exception(u; v) exception(u; v)

  BY exceptionRemainder ()
  
  H  ⊢ x ∈ ℤ

Rule: addAssociative
This rule proved as lemma rule_add_associative_true in file rules/rules_integer_ring.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ((m n) k) (m k) ∈ ℤ

  BY addAssociative ()
  
  H  ⊢ m ∈ ℤ
  H  ⊢ n ∈ ℤ
  H  ⊢ k ∈ ℤ

Rule: addCommutative
This rule proved as lemma rule_add_commutative_true in file rules/rules_integer_ring.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (m n) (n m) ∈ ℤ

  BY addCommutative ()
  
  H  ⊢ m ∈ ℤ
  H  ⊢ n ∈ ℤ

Rule: addInverse
This rule proved as lemma rule_add_inverse_true in file rules/rules_integer_ring.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (n (-n)) 0 ∈ ℤ

  BY addInverse ()
  
  H  ⊢ n ∈ ℤ

Rule: multiplyCommutative
This rule proved as lemma rule_mul_commutative_true in file rules/rules_integer_ring.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (m n) (n m) ∈ ℤ

  BY multiplyCommutative ()
  
  H  ⊢ m ∈ ℤ
  H  ⊢ n ∈ ℤ

Rule: addZero
This rule proved as lemma rule_add_zero_true in file rules/rules_integer_ring.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (0 n) n ∈ ℤ

  BY addZero ()
  
  H  ⊢ n ∈ ℤ

Rule: multiplyOne
This rule proved as lemma rule_mul_one_true in file rules/rules_integer_ring.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (1 n) n ∈ ℤ

  BY multiplyOne ()
  
  H  ⊢ n ∈ ℤ

Rule: multiplyAssociative
This rule proved as lemma rule_mul_associative_true in file rules/rules_integer_ring.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ((m n) k) (m k) ∈ ℤ

  BY multiplyAssociative ()
  
  H  ⊢ m ∈ ℤ
  H  ⊢ n ∈ ℤ
  H  ⊢ k ∈ ℤ

Rule: multiplyDistributive
This rule proved as lemma rule_mul_distributive_true in file rules/rules_integer_ring.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (m (n k)) ((m n) (m k)) ∈ ℤ

  BY multiplyDistributive ()
  
  H  ⊢ m ∈ ℤ
  H  ⊢ n ∈ ℤ
  H  ⊢ k ∈ ℤ

Rule: addMonotonic
H  ⊢ c < d

  BY addMonotonic ()
  
  H  ⊢ a < b
  H  ⊢ (c d ∈ ℤ) ∨ c < d

Rule: lessDiscrete
H  ⊢ a < b ∨ ((1 a) b ∈ ℤ)

  BY lessDiscrete ()
  
  H  ⊢ a < b

Rule: lessTrichotomy
H  ⊢ b ∈ ℤ

  BY lessTrichotomy ()
  
  H  ⊢ ¬a < b
  H  ⊢ ¬b < a

Rule: divideRemainderSum
H  ⊢ (((a ÷ b) b) (a rem b)) ∈ ℤ

  BY divideRemainderSum ()
  
  H  ⊢ a ∈ ℤ
  H  ⊢ b ≠ 0

Rule: remainderBounds1
H  ⊢ (0 ≤ (a rem b)) ∧ rem b < ext <Ax, Ax>

  BY remainderBounds1 ()
  
  H  ⊢ a ≥ 
  H  ⊢ b > 0

Rule: remainderBounds2
H  ⊢ (0 ≥ (a rem b) ) ∧ ((a rem b) > (-b)) ext <Ax, Ax>

  BY remainderBounds2 ()
  
  H  ⊢ a ≤ 0
  H  ⊢ b > 0

Rule: remainderBounds3
H  ⊢ (0 ≥ (a rem b) ) ∧ ((a rem b) > b) ext <Ax, Ax>

  BY remainderBounds3 ()
  
  H  ⊢ a ≤ 0
  H  ⊢ b < 0

Rule: remainderBounds4
H  ⊢ (0 ≤ (a rem b)) ∧ rem b < -b ext <Ax, Ax>

  BY remainderBounds4 ()
  
  H  ⊢ a ≥ 
  H  ⊢ b < 0

Rule: multiplyPositive
H  ⊢ 0 < b

  BY multiplyPositive ()
  
  H  ⊢ 0 < a
  H  ⊢ 0 < b

Rule: isAtom2ReduceTrue
H  ⊢ isatom2(z;a;b) a

  BY isAtom2ReduceTrue ()
  
  H  ⊢ z ∈ Atom2

Rule: exceptionAtomeq2
H  ⊢ if x=2 exception(u; v) then else exception(u; v)

  BY exceptionAtomeq2 ()
  
  H  ⊢ x ∈ Atom2

Rule: exceptionAtomeq1
H  ⊢ if x=1 exception(u; v) then else exception(u; v)

  BY exceptionAtomeq1 ()
  
  H  ⊢ x ∈ Atom1

Rule: atomn_eqReduceFalseSq
H  ⊢ if a=$n then else u

  BY atomn_eqReduceFalseSq ()
  
  H  ⊢ u
  H  ⊢ (a b ∈ Atom$n) ⟶ Void

Rule: isinrExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY isinrExceptionCases ()
  
  H  ⊢ is-exception(if is inr then else v)
  x:(t)↓ ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsinr
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (p)↓

  BY callbyvalueIsinr ()
  
  H  ⊢ 0 ≤ eval if is inr then else b; 0

Rule: isatom1ExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY isatom1ExceptionCases ()
  
  H  ⊢ is-exception(isatom1(t;u;v))
  x:(t)↓ ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsatom1
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (p)↓

  BY callbyvalueIsatom1 ()
  
  H  ⊢ 0 ≤ eval isatom1(p;a;b); 0

Rule: isatom2ExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY isatom2ExceptionCases ()
  
  H  ⊢ is-exception(isatom2(t;u;v))
  x:(t)↓ ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsatom2
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (p)↓

  BY callbyvalueIsatom2 ()
  
  H  ⊢ 0 ≤ eval isatom2(p;a;b); 0

Rule: atom1_eqExceptionCases
H  ⊢ b ∈ T

  BY atom1_eqExceptionCases ()
  
  H  ⊢ is-exception(if t=1 then else w)
  x:(t ∈ Atom1), y:(u ∈ Atom1) ⊢ b ∈ T
  x:(t ∈ Atom1), y:is-exception(u) ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: remainderExceptionCases
This rule proved as lemma rule_arith_exception_cases_true in file rules/rules_arith_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY remainderExceptionCases ()
  
  H  ⊢ is-exception(t rem u)
  x:(t ∈ ℤ), y:is-exception(u) ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueRemainder
This rule proved as lemma rule_callbyvalue_arith_true in file rules/rules_arith_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (a ∈ ℤ) ∧ (b ∈ ℤext <Ax, Ax>

  BY callbyvalueRemainder ()
  
  H  ⊢ 0 ≤ eval rem b; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: sqleIntensionalEquality
H  ⊢ (a ≤ b) (c ≤ d) ∈ Type

  BY sqleIntensionalEquality ()
     
     Let SubGoals CallLisp(SQLE-EQUALITY)
  SubGoals

Rule: exceptionAtomeq
H  ⊢ if x=exception(u; v) then else fi  exception(u; v)

  BY exceptionAtomeq ()
  
  H  ⊢ x ∈ Atom

Rule: atom_eqExceptionCases
H  ⊢ b ∈ T

  BY atom_eqExceptionCases ()
  
  H  ⊢ is-exception(if t=u then else fi )
  x:(t ∈ Atom), y:(u ∈ Atom) ⊢ b ∈ T
  x:(t ∈ Atom), y:is-exception(u) ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: atom_eqReduceFalseSq
H  ⊢ if a=b then else fi  u

  BY atom_eqReduceFalseSq ()
  
  H  ⊢ u
  H  ⊢ (a b ∈ Atom) ⟶ Void

Rule: atom_eqReduceTrueSq
H  ⊢ if a=b then else fi  u

  BY atom_eqReduceTrueSq ()
  
  H  ⊢ u
  H  ⊢ b ∈ Atom

Rule: bar_Induction
H  ⊢ c ∈ c

  BY bar_Induction !parameter{i:l} ()
     
     n,s can not occur free in B
  H  ⊢ T ∈ Type
  n:ℕs:(ℕn ⟶ T) ⊢ (B s) ∨ (B s))
  a:(ℕ ⟶ T) ⊢ ↓∃n:ℕ(B a)
  n:ℕs:(ℕn ⟶ T), x:B s ⊢ s ∈ s
  n:ℕs:(ℕn ⟶ T), x:(∀t:T
                             (f (n 1) m.if m=n  then t  else (s m)) ∈ (n 1) m.if m=n  then t  else (s m))))
     ⊢ s ∈ s

Rule: perfunctionExtensionality
H  ⊢ g ∈ per-function(A;x.B)

  BY perfunctionExtensionality !parameter{i:l} ()
  
  u:A ⊢ (f u) (g u) ∈ B[u/x]
  H  ⊢ A ∈ Type

Rule: sqequalnIntensionalEquality
H  ⊢ (a ~n b) (c ~m d) ∈ Type

  BY sqequalnIntensionalEquality ()
  
  H  ⊢ m ∈ ℕ
  H  ⊢ c ∈ Base
  H  ⊢ d ∈ Base

Rule: sqlenIntensionalEquality
H  ⊢ (a ≤b) (c ≤d) ∈ Type

  BY sqlenIntensionalEquality ()
  
  H  ⊢ m ∈ ℕ
  H  ⊢ c ∈ Base
  H  ⊢ d ∈ Base

Rule: sqlenSubtypeRel
x:(a ≤b), J ⊢ a ≤b

  BY sqlenSubtypeRel #$i
  
  H  ⊢ n ∈ ℕ

Rule: sqequalnSqlen
H  ⊢ ~n b

  BY sqequalnSqlen ()
  
  H  ⊢ a ≤b
  H  ⊢ b ≤a

Rule: sqequalnSymm
H  ⊢ ~n b

  BY sqequalnSymm ()
  
  H  ⊢ ~n a

Rule: sqntypeEquality
H  ⊢ (SqnType(T)) (SqmType(S)) ∈ Type

  BY sqntypeEquality ()
  
  H  ⊢ m ∈ ℕ
  H  ⊢ S ∈ Type

Rule: applyInr
This rule proved as lemma rule_apply_inr_true in file rules/rules_apply_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (inr b ≤ ⊥

  BY applyInr ()
  
  No Subgoals

Rule: applyInl
This rule proved as lemma rule_apply_inl_true in file rules/rules_apply_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (inl a) b ≤ ⊥

  BY applyInl ()
  
  No Subgoals

Rule: applyPair
This rule proved as lemma rule_apply_pair_true in file rules/rules_apply_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ <a, b> c ≤ ⊥

  BY applyPair ()
  
  No Subgoals

Rule: bottomDivergent
This rule proved as lemma rule_bottom_diverges_true3 in file rules/rules_false.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ¬(⊥)↓

  BY bottomDiverges ()
  
  No Subgoals

Rule: isinlExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY isinlExceptionCases ()
  
  H  ⊢ is-exception(if is inl then else v)
  x:(t)↓ ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsinl
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (p)↓

  BY callbyvalueIsinl ()
  
  H  ⊢ 0 ≤ eval if is inl then else b; 0

Rule: isintExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY isintExceptionCases ()
  
  H  ⊢ is-exception(if is an integer then else v)
  x:(t)↓ ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsint
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (p)↓

  BY callbyvalueIsint ()
  
  H  ⊢ 0 ≤ eval if is an integer then else b; 0

Rule: isatomExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY isatomExceptionCases ()
  
  H  ⊢ is-exception(if is an atom then otherwise v)
  x:(t)↓ ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsatom
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (p)↓

  BY callbyvalueIsatom ()
  
  H  ⊢ 0 ≤ eval if is an atom then otherwise b; 0

Rule: imageEqInduction
y:(t2 (f t1) ∈ Image(A,f)), J ⊢ t2 (f t1) ∈ T

  BY imageEqInduction #$i ()
  
  H  ⊢ f ∈ Base
  H  ⊢ t1 ∈ A
  H  ⊢ t1 ∈ T
  a:Base, b:Base, y:(f a ∈ T), z:(a b ∈ A) ⊢ (f a) (f b) ∈ T

Rule: tryReduceValue
This rule proved as lemma rule_try_reduce_value_true in file rules/rules_exception2.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ t1?n:x.t2 if n=2 then t1 else ⊥

  BY tryReduceValue ()
  
  H  ⊢ 0 ≤ eval t1; 0

Rule: callbyvalueAtomEq
H  ⊢ (a ∈ Atom) ∧ (b ∈ Atom) ext <Ax, Ax>

  BY callbyvalueAtomEq ()
  
  H  ⊢ 0 ≤ eval if a=b then else fi 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: pertypeEquality
This rule proved as lemma rule_pertype_equality_true in file rules/rules_pertype.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ pertype(R) pertype(R') ∈ Type

  BY pertypeEquality ()
  
  x:Base, y:Base ⊢ y ∈ Type
  x:Base, y:Base ⊢ R' y ∈ Type
  x:Base, y:Base, z:R y ⊢ R' y
  x:Base, y:Base, z:R' y ⊢ y
  x:Base, y:Base, z:R y ⊢ x
  x:Base, y:Base, z:Base, u:R y, v:R z ⊢ z

Rule: sqleExtensionalEquality
This rule proved as lemma rule_approx_extensional_equality_true in file rules/rules_squiggle4.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (a ≤ b) (c ≤ d) ∈ Type

  BY sqleExtensionalEquality ()
  
  H  ⊢ ↓a ≤ ⇐⇒ c ≤ d

Rule: sqntypeDef
H  ⊢ ~n y

  BY sqntypeDef ()
  
  H  ⊢ y ∈ T
  H  ⊢ SqnType(T)

Rule: sqntypeIntro
H  ⊢ SqnType(T)

  BY sqntypeIntro !parameter{i:l} ()
  
  x:T, y:T, u:(x y ∈ T) ⊢ ~n y
  H  ⊢ T ∈ Type

Rule: exceptionInteq
H  ⊢ if x=exception(u; v)  then y  else exception(u; v)

  BY exceptionInteq ()
  
  H  ⊢ x ∈ ℤ

Rule: exceptionAdd
This rule proved as lemma rule_exception_arith_true3 in file rules/rules_arith_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (exception(u; v)) exception(u; v)

  BY exceptionAdd ()
  
  H  ⊢ x ∈ ℤ

Rule: StrongSquashedBarInduction
H  ⊢ ↓seq-normalize(0;t)

  BY StrongSquashedBarInduction !parameter{i:l} ()
     
     n,s can not occur free in B
  n:ℕs:(ℕn ⟶ ℕ) ⊢ s ∈ Type
  n:ℕs:(ℕn ⟶ ℕ) ⊢ s ∈ Type
  H  ⊢ t
  s:(ℕ ⟶ ℕ), w:(⋂m:ℕ(↓s)) ⊢ ↓∃n:ℕ(B s)
  n:ℕs:(ℕn ⟶ ℕ), z:(↓s), w:B s ⊢ s
  n:ℕs:(ℕn ⟶ ℕ), z:(↓s), w:(⋂m:ℕ
                                         ↓(n 1) x.if x=n  then m  else (s x)) 
                                         supposing ↓(n 1) x.if x=n  then m  else (s x)))
     ⊢ s

Rule: isaxiomCases
This rule proved as lemma rule_isaxiom_cases_true in file rules/rules_axiom_cases.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ext !((!\\x.if Ax then ea otherwise eb) Ax)

  BY isaxiomCases ()
  
  H  ⊢ 0 ≤ eval in 0
  H  ⊢ t ∈ Base
  x:(t Ax) ⊢ ext ea
  x:(∀[u,v:Base].  (if Ax then otherwise v)) ⊢ ext eb

Rule: isaxiomExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY isaxiomExceptionCases ()
  
  H  ⊢ is-exception(if Ax then otherwise v)
  x:(t)↓ ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsaxiom
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (p)↓

  BY callbyvalueIsaxiom ()
  
  H  ⊢ 0 ≤ eval if Ax then otherwise b; 0

Rule: sqleTransitivity
This rule proved as lemma rule_approx_trans_true3 in file rules/rules_squiggle8.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ a ≤ b

  BY sqleTransitivity t
  
  H  ⊢ a ≤ t
  H  ⊢ t ≤ b

Rule: exceptionCompactness
z:(exception(u; v) ≤ fix(f)), J ⊢ ext !((!\\x.g) Ax)

  BY exceptionCompactness #$i ()
  
  z:(exception(u; v) ≤ fix(f)), [j:ℕ], x:(exception(u; v) ≤ (f^j ⊥)), J ⊢ ext g

Rule: isinrCases
This rule proved as lemma rule_isinr_cases_true in file rules/rules_inl_inr_cases.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ext !((!\\x.if is inr then ea else eb) Ax)

  BY isinrCases ()
  
  H  ⊢ 0 ≤ eval in 0
  H  ⊢ t ∈ Base
  x:(t inr outr(t) ) ⊢ ext ea
  x:(∀[u,v:Base].  (if is inr then else v)) ⊢ ext eb

Rule: isinlCases
This rule proved as lemma rule_isinl_cases_true in file rules/rules_inl_inr_cases.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ext !((!\\x.if is inl then ea else eb) Ax)

  BY isinlCases ()
  
  H  ⊢ 0 ≤ eval in 0
  H  ⊢ t ∈ Base
  x:(t inl outl(t)) ⊢ ext ea
  x:(∀[u,v:Base].  (if is inl then else v)) ⊢ ext eb

Rule: freeFromAtom1Atom2
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ a#x:Atom2

  BY freeFromAtom1Atom2 ()
  
  H  ⊢ x ∈ Atom2

Rule: StrongContinuity2
This rule proved as lemma rule_strong_continuity_true2_v3_2 in file continuity/stronger_continuity_rule4_v3.v
 at https://github.com/vrahli/NuprlInCoq  


   ⊢ <λn,f. ν(v.F x.if (x) < (0)  then ⊥  else if (x) < (n)  then x  else (exception(v; Ax)))?v:x.Ax), λf.<Ax, λn.Ax\000C>>
     ∈ ⇃(∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ Unit)
          ∀f:ℕ ⟶ T
            ((↓∃n:ℕ((M f) (F f) ∈ ℕ))
            ∧ (∀n:ℕ(M f) (F f) ∈ ℕ supposing if is an integer then True else False)))

  BY StrongContinuity2 ()
  
  H  ⊢ F ∈ (ℕ ⟶ T) ⟶ ℕ
  H  ⊢ ↓T
  H  ⊢ T ⊆r ℕ

Rule: SquashedBarInductionSqBase
H  ⊢ ↓seq-normalize(0;t)

  BY SquashedBarInductionSqBase !parameter{i:l} ()
     
     n,s can not occur free in B
  n:ℕs:(ℕn ⟶ ℕ) ⊢ s ∈ Type
  s:(ℕ ⟶ ℕ) ⊢ ↓∃n:ℕ(B seq-normalize(n;s))
  n:ℕs:(ℕn ⟶ ℕ), w:(↓s) ⊢ s
  n:ℕs:(ℕn ⟶ ℕ), w:(∀m:ℕ(P (n 1) x.if x=n  then m  else (s x)))) ⊢ s

Rule: SquashedBarInduction
H  ⊢ ↓seq-normalize(0;t)

  BY SquashedBarInduction !parameter{i:l} ()
     
     n,s can not occur free in B
  n:ℕs:(ℕn ⟶ ℕ) ⊢ s ∈ Type
  s:(ℕ ⟶ ℕ) ⊢ ↓∃n:ℕ(B seq-normalize(n;s))
  n:ℕs:(ℕn ⟶ ℕ), w:B s ⊢ s
  n:ℕs:(ℕn ⟶ ℕ), w:(∀m:ℕ(P (n 1) x.if x=n  then m  else (s x)))) ⊢ s

Rule: choiceSequenceRec
H  ⊢ ↓∃f:ℕ ⟶ ℕ. ∀n:ℕ(↓f)

  BY choiceSequenceRec !parameter{i:l} ()
     
     n ≠ 
     f ≠ 
     m ≠ 
     x ≠ 
     x ≠ 
     x ≠ 
     can not occur free in P
  H  ⊢ s
  n:ℕf:(ℕn ⟶ ℕ), z:P f ⊢ ↓∃m:ℕ(P (n 1) x.if x=n  then m  else (f x)))
  n:ℕf:(ℕn ⟶ ℕ) ⊢ f ∈ Type

Rule: classicalIntroduction
This rule proved as lemma rule_classical_introduction_true3 in file rules/rules_classical.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ {x:Unit| P} 

  BY classicalIntroduction !parameter{i:l} ()
  
  H  ⊢ P ∈ Type
  z:(P ⟶ Void) @i ⊢ Void

Rule: parameterizedRecEquality
H  ⊢ pRec(C1;x1.B1;c1) pRec(C2;x2.B2;c2) ∈ Type

  BY parameterizedRecEquality ()
     
     
  x:(C1 ⟶ Type) ⊢ B1[x/x1] B2[x/x2] ∈ (C1 ⟶ Type)
  x:(C1 ⟶ Type), y:(C1 ⟶ Type), z:(∀c:C1. ((x c) ⊆(y c))) ⊢ ∀c:C1. ((B1[x/x1] c) ⊆(B2[y/x2] c))
  H  ⊢ C1 C2 ∈ Type
  H  ⊢ c1 c2 ∈ C1

Rule: dependentIntersectionEquality
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ x1:a1 ⋂ b1 x2:a2 ⋂ b2 ∈ Type

  BY dependentIntersectionEquality y
  
  H  ⊢ a1 a2 ∈ Type
  y:a1 ⊢ b1[y/x1] b2[y/x2] ∈ Type

Rule: ispairExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY ispairExceptionCases ()
  
  H  ⊢ is-exception(if is pair then otherwise v)
  x:(t)↓ ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIspair
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (p)↓

  BY callbyvalueIspair ()
  
  H  ⊢ 0 ≤ eval if is pair then otherwise b; 0

Rule: exceptionLess
H  ⊢ if (x) < (exception(u; v))  then y  else exception(u; v)

  BY exceptionLess ()
  
  H  ⊢ x ∈ ℤ

Rule: strong_bar_Induction
H  ⊢ c ∈ c

  BY strong_bar_Induction !parameter{i:l} con ()
  
  H  ⊢ T ∈ Type
  n:ℕs:(ℕn ⟶ T), t:T ⊢ t ∈ Type
  n:ℕs:(ℕn ⟶ T), con:(∀x:ℕn. (R (s x))) ⊢ (B s) ∨ (B s))
  a:(ℕ ⟶ T), con:(∀n:ℕ(R (a n))) ⊢ ↓∃n:ℕ(B a)
  n:ℕs:(ℕn ⟶ T), con:(∀x:ℕn. (R (s x))), m:B s ⊢ s ∈ s
  n:ℕs:(ℕn ⟶ T), con:(∀x:ℕn. (R (s x))), x:(∀t:{t:T| t} 
                                                         (f (n 1) m.if m=n  then t  else (s m)) ∈ (n 1) 
                                                                                                      m.if m=n
                                                                                                             then t
                                                                                                             else (s 
                                                                                                                   m))))
     ⊢ s ∈ s

Rule: pertypeMemberEquality
This rule proved as lemma rule_pertype_member_equality_true in file rules/rules_pertype.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ t1 t2 ∈ pertype(R)

  BY pertypeMemberEquality !parameter{i:l}
  
  H  ⊢ pertype(R) ∈ Type
  H  ⊢ t1 t2
  H  ⊢ t1 ∈ Base
  H  ⊢ t2 ∈ Base

Rule: islambdaExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY islambdaExceptionCases ()
  
  H  ⊢ is-exception(if is lambda then otherwise v)
  x:(t)↓ ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: sqleLambda
H  ⊢ ~ λx.(f x)

  BY sqleLambda ()
     
     can not occur free in f
  H  ⊢ f ≤ λy.a
  H  ⊢ (f)↓

Rule: exceptionApplyCases
This rule proved as lemma rule_apply_exception_cases_true in file rules/rules_apply_exception_cases_true.v
 at https://github.com/vrahli/NuprlInCoq  


   ⊢ ↓(exception(⊥; ⊥) ≤ f)
      ∨ (f ~ λx.(f x))
      ∨ (⋂x:Base. ⋂z:(x)↓.  if is an integer then True else x ≤ ⊥ext islambda(f)

  BY exceptionApplyCases ()
     
     x ≠ 
     x,z can not occur free in f
  H  ⊢ exception(⊥; ⊥) ≤ a
  H  ⊢ f ∈ Base

Rule: callbyvalueApplyCases
This rule proved as lemma rule_callbyvalue_apply_cases_true in file rules/rules_apply_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (f ~ λx.(f x)) ∨ (⋂x:Base. ⋂z:(x)↓.  if is an integer then True else x ≤ ⊥ext islambda(f)

  BY callbyvalueApplyCases ()
     
     x ≠ 
     x,z can not occur free in f
  H  ⊢ 0 ≤ eval a; 0
  H  ⊢ f ∈ Base

Rule: callbyvalueIslambda
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (p)↓

  BY callbyvalueIslambda ()
  
  H  ⊢ 0 ≤ eval if is lambda then otherwise b; 0

Rule: sqequalExtensionalEquality
This rule proved as lemma rule_cequiv_extensional_equality_true in file rules/rules_squiggle4.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (a b) (c d) ∈ Type

  BY sqequalExtensionalEquality ()
  
  H  ⊢ ↓⇐⇒ d

Rule: islambdaCases
H  ⊢ ext !((!\\x.if is lambda then ea otherwise eb) Ax)

  BY islambdaCases ()
  
  H  ⊢ 0 ≤ eval in 0
  H  ⊢ t ∈ Base
  x:(t ~ λu.(t u)) ⊢ ext ea
  x:(∀[u,v:Base].  (if is lambda then otherwise v)) ⊢ ext eb

Rule: isect_member_caseEquality
H  ⊢ f1 f2 ∈ B[a1/x]

  BY isect_member_caseEquality (⋂x:A. B) a1 ()
  
  H  ⊢ f1 f2 ∈ (⋂x:A. B)
  H  ⊢ a1 a1 ∈ A

Rule: token1Equality
H  ⊢ '$x'1 '$x'1 ∈ Atom1

  BY token1Equality ()
  
  No Subgoals

Rule: barInduction
H  ⊢ [] ∈ []

  BY barInduction !parameter{i:l} ()
  
  H  ⊢ T ∈ Type
  s:(T List) ⊢ (R s) ∨ (R s))
  a:(ℕ ⟶ T) ⊢ ↓∃n:ℕ(R map(a;upto(n)))
  s:(T List), x:R s ⊢ s ∈ s
  s:(T List), x:(∀t:T. (f (s [t]) ∈ (s [t]))) ⊢ s ∈ s

Rule: isintReduceAtom
H  ⊢ if is an integer then else b

  BY isintReduceAtom ()
  
  H  ⊢ z ∈ Atom

Rule: ispairCases
This rule proved as lemma rule_ispair_cases_true in file rules/rules_cft.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ext !((!\\x.if is pair then ea otherwise eb) Ax)

  BY ispairCases ()
  
  H  ⊢ 0 ≤ eval in 0
  H  ⊢ t ∈ Base
  x:(t ~ <fst(t), snd(t)>) ⊢ ext ea
  x:(∀[u,v:Base].  (if is pair then otherwise v)) ⊢ ext eb

Rule: isintCases
H  ⊢ ext !((!\\x.if is an integer then ea else eb) Ax)

  BY isintCases ()
  
  H  ⊢ 0 ≤ eval in 0
  H  ⊢ t ∈ Base
  x:(t ∈ ℤ) ⊢ ext ea
  x:(∀[u,v:Base].  (if is an integer then else v)) ⊢ ext eb

Rule: isatomReduceTrue
H  ⊢ if is an atom then otherwise a

  BY isatomReduceTrue ()
  
  H  ⊢ z ∈ Atom

Rule: sqlenSqequaln
H  ⊢ a ≤b

  BY sqlenSqequaln ()
  
  H  ⊢ ~n b

Rule: sqle_n rule
H  ⊢ a ≤b

  BY sqle_n ()
     
     Let SubGoals CallLisp(SQLE-N)
  SubGoals

Rule: divergentSqlen
H  ⊢ a ≤b

  BY divergentSqlen !parameter{i:l} ()
  
  y:(a)↓ ⊢ a ≤b
  y:is-exception(a) ⊢ a ≤b
  H  ⊢ (a)↓ ∈ ℙ

Rule: sqleZero
H  ⊢ a ≤b

  BY sqleZero ()
  
  No Subgoals

Rule: axiomSqleNEquality
H  ⊢ Ax Ax ∈ (a ≤b)

  BY axiomSqleNEquality ()
  
  H  ⊢ a ≤b

Rule: sqleDefinition
H  ⊢ a ≤ b

  BY sqleDefinition n
  
  n:ℕ ⊢ a ≤b

Rule: compactness
z:(F fix(f))↓J ⊢ ext !((!\\x.g) Ax)

  BY compactness #$i ()
  
  z:(F fix(f))↓[j:ℕ], x:(F (f^j ⊥))↓J ⊢ ext g

Rule: randomEquality
H  ⊢ random(p1;a1;b1) random(p2;a2;b2) ∈ (ℕ ⟶ Outcome)

  BY randomEquality ()
  
  H  ⊢ p1 p2 ∈ FinProbSpace
  H  ⊢ a1 a2 ∈ Atom$n
  H  ⊢ b1 b2 ∈ Atom$n

Rule: findRandomEquality
H  ⊢ find-random{$k}(C1;p1;a1;b1) find-random{$k}(C2;p2;a2;b2) ∈ {n:ℕ(C <n, random(p;a;b)>1 ∈ ℤ

  BY findRandomEquality ()
  
  H  ⊢ p1 p2 ∈ FinProbSpace
  H  ⊢ a1 a2 ∈ Atom$k
  H  ⊢ b1 b2 ∈ Atom$k
  H  ⊢ C1 C2 ∈ p-open(p1)
  H  ⊢ measure(C1) 1
  H  ⊢ a1#C1:p-open(p1) ∨ b1#C1:p-open(p1)

Rule: multiplyExceptionCases
This rule proved as lemma rule_arith_exception_cases_true in file rules/rules_arith_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY multiplyExceptionCases ()
  
  H  ⊢ is-exception(t u)
  x:(t ∈ ℤ), y:is-exception(u) ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueMultiply
This rule proved as lemma rule_callbyvalue_arith_true in file rules/rules_arith_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (a ∈ ℤ) ∧ (b ∈ ℤext <Ax, Ax>

  BY callbyvalueMultiply ()
  
  H  ⊢ 0 ≤ eval b; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: int_eqExceptionCases
H  ⊢ b ∈ T

  BY int_eqExceptionCases ()
  
  H  ⊢ is-exception(if t=u  then z  else w)
  x:(t ∈ ℤ), y:(u ∈ ℤ) ⊢ b ∈ T
  x:(t ∈ ℤ), y:is-exception(u) ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueIntEq
H  ⊢ (a ∈ ℤ) ∧ (b ∈ ℤext <Ax, Ax>

  BY callbyvalueIntEq ()
  
  H  ⊢ 0 ≤ eval if a=b  then u  else v; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: lessExceptionCases
This rule proved as lemma rule_less_exception_cases_true in file rules/rules_less_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY lessExceptionCases ()
  
  H  ⊢ is-exception(if (t) < (u)  then z  else w)
  x:(t ∈ ℤ), y:(u ∈ ℤ) ⊢ b ∈ T
  x:(t ∈ ℤ), y:is-exception(u) ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueLess
H  ⊢ (a ∈ ℤ) ∧ (b ∈ ℤext <Ax, Ax>

  BY callbyvalueLess ()
  
  H  ⊢ 0 ≤ eval if (a) < (b)  then u  else v; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: divideExceptionCases
This rule proved as lemma rule_arith_exception_cases_true in file rules/rules_arith_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY divideExceptionCases ()
  
  H  ⊢ is-exception(t ÷ u)
  x:(t ∈ ℤ), y:is-exception(u) ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueDivide
This rule proved as lemma rule_callbyvalue_arith_true in file rules/rules_arith_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (a ∈ ℤ) ∧ (b ∈ ℤext <Ax, Ax>

  BY callbyvalueDivide ()
  
  H  ⊢ 0 ≤ eval a ÷ b; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: minusExceptionCases
This rule proved as lemma rule_minus_exception_cases_true in file rules/rules_arith_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY minusExceptionCases ()
  
  H  ⊢ is-exception(-t)
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueMinus
This rule proved as lemma rule_callbyvalue_minus_true in file rules/rules_arith_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ a ∈ ℤ

  BY callbyvalueMinus ()
  
  H  ⊢ 0 ≤ eval -a; 0
  H  ⊢ a ∈ Base

Rule: Continuity
This rule proved as lemma rule_continuity_true3 in file continuity/continuity_rule_gen.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ↓∃n:ℕ. ∀[g:ℤ ⟶ ℤ]. (F f) (F g) ∈ ℤ supposing ∀[i:ℤ]. (f i) (g i) ∈ ℤ supposing |i| < n

  BY Continuity ()
  
  H  ⊢ F ∈ (ℤ ⟶ ℤ) ⟶ ℤ
  H  ⊢ f ∈ ℤ ⟶ ℤ

Rule: isintReduceTrue
This rule proved as lemma rule_isint_reduce_true_true3 in file rules/rules_isint.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ if is an integer then else a

  BY isintReduceTrue ()
  
  H  ⊢ z ∈ ℤ

Rule: cutEval
J ⊢ ext eval in t

  BY cutEval #$i x
  
  J ⊢ ext s
  J ⊢ value-type(S)
  x:S, J ⊢ ext t

Rule: uallLevelFunctionality
x:(∀[x1:T]. P ∈ 𝕌{lvl}), J ⊢ ∀[x2:T]. Q ∈ 𝕌{lvl} ext experimental{uallLevelFunctionality}(Ax)

  BY uallLevelFunctionality #$i ()
  
  v:T @lvl, w:P ∈ 𝕌{lvl}[v/x1], J ⊢ Q ∈ 𝕌{lvl}[v/x2]

Rule: remainderEquality
This rule proved as lemma rule_arithop_equality_true3 in file rules/rules_arith.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (m1 rem n1) (m2 rem n2) ∈ ℤ

  BY remainderEquality ()
  
  H  ⊢ m1 m2 ∈ ℤ
  H  ⊢ n1 n2 ∈ ℤ
  H  ⊢ n1 ≠ 0

Rule: pointwiseFunctionalityForEquality
This rule proved as lemma rule_functionaliy_for_equality_true in file rules/rules_functionality.v
 at https://github.com/vrahli/NuprlInCoq  

a:A, J ⊢ t1 t2 ∈ T

  BY pointwiseFunctionalityForEquality #$i !parameter{j:l} ()
  
  a:A, J ⊢ T ∈ 𝕌{j}
  a:Base, b:Base, z:(a b ∈ A), J ⊢ t1 t2[b/a] ∈ T

Rule: equalityUniverseElim
This rule proved as lemma rule_equality_universe_elim_true in file rules/rules_equality.v
 at https://github.com/vrahli/NuprlInCoq  

x:((x1 y1 ∈ A1) (x2 y2 ∈ A2) ∈ Type), J ⊢ ext e

  BY equalityUniverseElim #$n ()
  
  x:((x1 y1 ∈ A1) (x2 y2 ∈ A2) ∈ Type), [y:(A1 A2 ∈ Type)], [z:(x1 x2 ∈ (A1 ⋃ Base))], [w:(y1
    y2
    ∈ (A1 ⋃ Base))], J
     ⊢ ext e

Rule: functionUniverseElim
z:((z1:A1 ⟶ B1) (z2:A2 ⟶ B2) ∈ Type), J ⊢ ext e

  BY functionUniverseElim #$h ()
  
  z:((z1:A1 ⟶ B1) (z2:A2 ⟶ B2) ∈ Type), [x:(A1 A2 ∈ Type)], [y:(∀a:A1. (B1[a/z1] B2[a/z2] ∈ Type))], J
     ⊢ ext e

Rule: pointwiseFunctionality wrename
x:A, J ⊢ ext t

  BY pointwiseFunctionalityWR #$i !parameter{j:l} vs ()
  
  [x:Base], [z:(x ∈ A)], J ⊢ ext t
  x:Base, y:Base, z:(x y ∈ A), J, !subgoal_equations(x.J; vs; x; y) ⊢ C[y/x] ∈ 𝕌{j}

Rule: sqequalElimination
x:(p q), J ⊢ ext t

  BY sqequalElimination #$i
  
  x:(p q), J[Ax/x] ⊢ C[Ax/x] ext t

Rule: sqequalZero
H  ⊢ ~0 b

  BY sqequalZero ()
  
  No Subgoals

Rule: sqequalnReflexivity
H  ⊢ ~n a

  BY sqequalnReflexivity ()
  
  H  ⊢ n ∈ ℕ

Rule: sqequal_n rule
H  ⊢ ~n b

  BY sqequal_n ()
     
     Let SubGoals CallLisp(SQEQUAL-N)
  SubGoals

Rule: sqequalDefinition
H  ⊢ b

  BY sqequalDefinition n
  
  n:ℕ ⊢ ~n b

Rule: fixpointLeast
H  ⊢ F[fix(f)/z] ≤ t

  BY fixpointLeast ()
  
  j:ℕ ⊢ F[f^j ⊥/z] ≤ t

Rule: sqleRule
H  ⊢ a ≤ ext t

  BY sqle ()
     
     Let SubGoals CallLisp(SQLE)
  SubGoals

Rule: spreadExceptionCases
This rule proved as lemma rule_spread_exception_cases_true in file rules/rules_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY spreadExceptionCases y,z.u ()
  
  H  ⊢ is-exception(let y,z in u)
  x:(t ∈ Top × Top) ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueSpread
This rule proved as lemma rule_halt_spread_true in file rules/rules_halts_spread.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ p ∈ Top × Top

  BY callbyvalueSpread y,z.a ()
  
  H  ⊢ 0 ≤ eval let y,z in a; 0

Rule: atom2_eqExceptionCases
H  ⊢ b ∈ T

  BY atom2_eqExceptionCases ()
  
  H  ⊢ is-exception(if t=2 then else w)
  x:(t ∈ Atom2), y:(u ∈ Atom2) ⊢ b ∈ T
  x:(t ∈ Atom2), y:is-exception(u) ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueAtomnEq
H  ⊢ (a ∈ Atom$n) ∧ (b ∈ Atom$n) ext <Ax, Ax>

  BY callbyvalueAtomnEq ()
  
  H  ⊢ 0 ≤ eval if a=$n then else v; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: applyExceptionCases
This rule proved as lemma rule_isexc_apply_cases_true in file rules/rules_apply_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY applyExceptionCases ()
  
  H  ⊢ is-exception(t u)
  x:(t)↓ ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueApply
This rule proved as lemma rule_callbyvalue_apply_true in file rules/rules_apply_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (f)↓

  BY callbyvalueApply ()
  
  H  ⊢ 0 ≤ eval a; 0

Rule: callbyvalueExceptionCases
This rule proved as lemma rule_cbv_exception_cases_true in file rules/rules_cbv_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY callbyvalueExceptionCases y.u ()
  
  H  ⊢ is-exception(eval in u)
  x:(t)↓ ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueCallbyvalue
This rule proved as lemma rule_callbyvalue_cbv_true in file rules/rules_cft_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (a)↓

  BY callbyvalueCallbyvalue z.b ()
  
  H  ⊢ 0 ≤ eval eval in b; 0

Rule: uallFunctionality
f:(∀[x1:T]. P) @lvl, J ⊢ ∀[x2:T]. ext experimental{uallFunctionality}(λv.((λw.t) f))

  BY uallFunctionality #$i ()
  
  [v:T] @lvl, w:P[v/x1] @lvl, J ⊢ Q[v/x2] ext t

Rule: sqequalIntensionalEquality
H  ⊢ (a b) (c d) ∈ Type

  BY sqequalIntensionalEquality ()
  
  H  ⊢ c ∈ Base
  H  ⊢ d ∈ Base

Rule: dependent_set_memberFormation
This rule proved as lemma rule_dependent_set_member_formation_true in file rules/rules_set.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ {x:A| B}  ext a

  BY dependent_set_memberFormation !parameter{i:l} ()
  
  H  ⊢ a ∈ A
  H  ⊢ B[a/x]
  y:A ⊢ B[y/x] B[y/x] ∈ Type

Rule: pertypeElimination
This rule proved as lemma rule_pertype_elimination_t_true in file rules/rules_pertype.v
 at https://github.com/vrahli/NuprlInCoq  

x:(t1 t2 ∈ pertype(R)), J ⊢ ext e

  BY pertypeElimination #$n !parameter{i:l} ()
  
  x:(t1 t2 ∈ pertype(R)), [y:R t1 t2], J ⊢ ext e
  x:(t1 t2 ∈ pertype(R)), J ⊢ t1 t2 ∈ Type

Rule: token2Equality
H  ⊢ '$x'2 '$x'2 ∈ Atom2

  BY token2Equality ()
  
  No Subgoals

Rule: freeFromAtomSet
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ a#x:{v:T| P} 

  BY freeFromAtomSet ()
  
  H  ⊢ a#x:T
  H  ⊢ x ∈ {v:T| P} 

Rule: freeFromAtomAxiom
H  ⊢ Ax Ax ∈ a#x:T

  BY freeFromAtomAxiom ()
  
  H  ⊢ a#x:T

Rule: freeFromAtomBase
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ a#x:Atom$n

  BY freeFromAtomBase ()
  
  H  ⊢ ¬(x a ∈ Atom$n)

Rule: atomn_eqReduceTrueSq
H  ⊢ if a=$n then else u

  BY atomn_eqReduceTrueSq ()
  
  H  ⊢ u
  H  ⊢ b ∈ Atom$n

Rule: freeFromAtomAbsurdity
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
 at https://github.com/vrahli/NuprlInCoq  

z:a#a:Atom$n, J ⊢ ext any z

  BY freeFromAtomAbsurdity #$i
  
  No Subgoals

Rule: freeFromAtomTriviality
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ a#x:T

  BY freeFromAtomTriviality ()
     
     !call_lisp_wargs{NO-UT-OCCURS:t}($n:n ())
  H  ⊢ x ∈ T

Rule: freeFromAtomApplication
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ a#f x:B[x/v]

  BY freeFromAtomApplication v:A ⟶ B
  
  H  ⊢ a#f:v:A ⟶ B
  H  ⊢ a#x:A

Rule: int_eqReduceFalseSq
H  ⊢ if a=b  then s  else u

  BY int_eqReduceFalseSq ()
  
  H  ⊢ u
  H  ⊢ (a b ∈ ℤ) ⟶ Void

Rule: int_eqReduceTrueSq
H  ⊢ if a=b  then s  else u

  BY int_eqReduceTrueSq ()
  
  H  ⊢ u
  H  ⊢ b ∈ ℤ

Rule: lessCases
H  ⊢ ext !((!\\x.if (t1) < (t2)  then ea  else eb) Ax)

  BY lessCases t1 t2 ()
  
  H  ⊢ t1 ∈ ℤ
  H  ⊢ t2 ∈ ℤ
  x:(∀[u,v:Base].  (if (t1) < (t2)  then u  else u)) ⊢ ext ea
  x:(∀[u,v:Base].  (if (t1) < (t2)  then u  else v)) ⊢ ext eb

Rule: lessEquality
H  ⊢ if (a1) < (b1)  then s1  else t1 if (a2) < (b2)  then s2  else t2 ∈ T

  BY lessEquality v
  
  H  ⊢ a1 a2 ∈ ℤ
  H  ⊢ b1 b2 ∈ ℤ
  v:a1 < b1 ⊢ s1 s2 ∈ T
  v:(a1 < b1 ⟶ Void) ⊢ t1 t2 ∈ T

Rule: atomnEquality
H  ⊢ Atom$n Atom$n ∈ Type

  BY atomnEquality ()
  
  No Subgoals

Rule: divergentSqle
This rule proved as lemma rule_convergence_true3 in file rules/rules_squiggle3.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ a ≤ b

  BY divergentSqle !parameter{i:l} ()
  
  y:(a)↓ ⊢ a ≤ b
  y:is-exception(a) ⊢ a ≤ b
  H  ⊢ (a)↓ ∈ ℙ
  H  ⊢ is-exception(a) ∈ ℙ

Rule: sqequalSqle
This rule proved as lemma rule_cequiv_approx_true3 in file rules/rules_squiggle.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b

  BY sqequalSqle ()
  
  H  ⊢ a ≤ b
  H  ⊢ b ≤ a

Rule: atom_eqEquality
H  ⊢ if a1=b1 then s1 else t1 fi  if a2=b2 then s2 else t2 fi  ∈ T

  BY atom_eqEquality v
  
  H  ⊢ a1 a2 ∈ Atom
  H  ⊢ b1 b2 ∈ Atom
  v:(a1 b1 ∈ Atom) ⊢ s1 s2 ∈ T
  v:((a1 b1 ∈ Atom) ⟶ Void) ⊢ t1 t2 ∈ T

Rule: dependent_pairEquality
This rule proved as lemma rule_pair_equality_true in file rules/rules_product.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ <a1, b1> = <a2, b2> ∈ (x:A × B)

  BY dependent_pairEquality !parameter{i:l} ()
  
  H  ⊢ a1 a2 ∈ A
  H  ⊢ b1 b2 ∈ B[a1/x]
  y:A ⊢ B[y/x] B[y/x] ∈ Type

Rule: dependentIntersection_memberEquality
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b1 b2 ∈ x:A ⋂ B

  BY dependentIntersection_memberEquality ()
  
  H  ⊢ b1 b2 ∈ A
  H  ⊢ b1 b2 ∈ B[b1/x]

Rule: dependentIntersectionEqElimination
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
 at https://github.com/vrahli/NuprlInCoq  

z:(a b ∈ x:A ⋂ B), J ⊢ ext !(!((!\\u.(!\\v.t)) Ax) Ax)

  BY dependentIntersectionEqElimination #$i ()
  
  z:(a b ∈ x:A ⋂ B), u:(a b ∈ A), v:(a b ∈ B[a/x]), J ⊢ ext t

Rule: dependentIntersectionElimination
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
 at https://github.com/vrahli/NuprlInCoq  

z:x:A ⋂ B, J ⊢ ext !(!((!\\u.(!\\v.t)) Ax) Ax)

  BY dependentIntersectionElimination #$i ()
  
  z:x:A ⋂ B, u:(z z ∈ A), v:(z z ∈ B[z/x]), J ⊢ ext t

Rule: axiomSqleEquality
This rule proved as lemma rule_approx_member_eq_true3 in file rules/rules_squiggle6.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ Ax Ax ∈ (a ≤ b)

  BY axiomSqleEquality ()
  
  H  ⊢ a ≤ b

Rule: minusEquality
This rule proved as lemma rule_minus_equality_true3 in file rules/rules_minus.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (-s) (-t) ∈ ℤ

  BY minusEquality ()
  
  H  ⊢ t ∈ ℤ

Rule: multiplyEquality
This rule proved as lemma rule_arithop_equality_true3 in file rules/rules_arith.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (m1 n1) (m2 n2) ∈ ℤ

  BY multiplyEquality ()
  
  H  ⊢ m1 m2 ∈ ℤ
  H  ⊢ n1 n2 ∈ ℤ

Rule: sqequalAxiom
This rule proved as lemma rule_cequiv_member_eq_true3 in file rules/rules_squiggle6.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ Ax Ax ∈ (a b)

  BY axiomSqEquality ()
  
  H  ⊢ b

Rule: callbyvalueReduce
This rule proved as lemma rule_callbyvalue_reduce_true3 in file rules_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  ⋅

H  ⊢ eval in t

  BY callbyvalueReduce ()
  
  H  ⊢ B[a/x] t
  H  ⊢ 0 ≤ eval in 0

Rule: addExceptionCases
This rule proved as lemma rule_arith_exception_cases_true in file rules/rules_arith_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY addExceptionCases ()
  
  H  ⊢ is-exception(t u)
  x:(t ∈ ℤ), y:is-exception(u) ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueAdd
This rule proved as lemma rule_callbyvalue_arith_true in file rules/rules_arith_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (a ∈ ℤ) ∧ (b ∈ ℤext <Ax, Ax>

  BY callbyvalueAdd ()
  
  H  ⊢ 0 ≤ eval b; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: decideEquality
H  ⊢ case e1 of inl(x1) => l1 inr(y1) => r1 case e2 of inl(x2) => l2 inr(y2) => r2 ∈ T[e1/z]

  BY decideEquality z.T (A B) ()
  
  H  ⊢ e1 e2 ∈ (A B)
  u:A, w:(e1 (inl u) ∈ (A B)) ⊢ l1[u/x1] l2[u/x2] ∈ T[inl u/z]
  v:B, w:(e1 (inr ) ∈ (A B)) ⊢ r1[v/y1] r2[v/y2] ∈ T[inr /z]

Rule: productUniverseElim
z:((z1:A1 × B1) (z2:A2 × B2) ∈ Type), J ⊢ ext e

  BY productUniverseElim #$h ()
  
  z:((z1:A1 × B1) (z2:A2 × B2) ∈ Type), [x:(A1 A2 ∈ Type)], [y:(∀a:A1. (B1[a/z1] B2[a/z2] ∈ Type))], J
     ⊢ ext e

Rule: unionUniverseElim
z:((A1 B1) (A2 B2) ∈ Type), J ⊢ ext e

  BY unionUniverseElim #$h ()
  
  z:((A1 B1) (A2 B2) ∈ Type), [x:(A1 A2 ∈ Type)], [y:(B1 B2 ∈ Type)], J ⊢ ext e

Rule: orLevelFunctionality
x:(P ∨ Q ∈ 𝕌{lvl}), J ⊢ A ∨ B ∈ 𝕌{lvl} ext experimental{orLevelFunctionality}(Ax)

  BY orLevelFunctionality #$i ()
  
  v:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}
  v:(Q ∈ 𝕌{lvl}), J ⊢ B ∈ 𝕌{lvl}

Rule: pointwiseFunctionality
This rule proved as lemma rule_functionaliy_true in file rules/rules_functionality.v
 at https://github.com/vrahli/NuprlInCoq  

z:A, J ⊢ ext t

  BY pointwiseFunctionality #$i !parameter{j:l} ()
  
  [a:Base], [b:Base], [c:(a b ∈ A)], J[a/z] ⊢ C[a/z] ext t
  a:Base, b:Base, c:(a b ∈ A), J[a/z] ⊢ C[a/z] C[b/z] ∈ 𝕌{j}

Rule: inrEquality
This rule proved as lemma rule_inr_equality_true in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (inr b1 (inr b2 ) ∈ (A B)

  BY inrEquality !parameter{i:l} ()
  
  H  ⊢ b1 b2 ∈ B
  H  ⊢ A ∈ Type

Rule: spreadEquality
This rule proved as lemma rule_spread_equality_true in file rules/rules_product.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ let x1,y1 e1 in t1 let x2,y2 e2 in t2 ∈ T[e1/z]

  BY spreadEquality z.T (w:A × B) ()
  
  H  ⊢ e1 e2 ∈ (w:A × B)
  u:A, v:B[u/w], a:(e1 = <u, v> ∈ (w:A × B)) ⊢ t1[u,v/x1,y1] t2[u,v/x2,y2] ∈ T[<u, v>/z]

Rule: andLevelFunctionality
x:(P ∧ Q ∈ 𝕌{lvl}), J ⊢ A ∧ B ∈ 𝕌{lvl} ext experimental{andLevelFunctionality}(Ax)

  BY andLevelFunctionality #$i ()
  
  v:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}
  v:P, w:(Q ∈ 𝕌{lvl}), J ⊢ B ∈ 𝕌{lvl}
  v:(P ∈ 𝕌{lvl}), w:A @lvl, J ⊢ P

Rule: existsLevelFunctionality
x:(∃x1:T. P ∈ 𝕌{lvl}), J ⊢ ∃x2:T. Q ∈ 𝕌{lvl} ext experimental{existsLevelFunctionality}(Ax)

  BY existsLevelFunctionality #$i ()
  
  v:T @lvl, w:P ∈ 𝕌{lvl}[v/x1], J ⊢ Q ∈ 𝕌{lvl}[v/x2]

Rule: existsFunctionality
p:(∃x1:T. P) @lvl, J ⊢ ∃x2:T. ext let v,w in <v, t>

  BY existsFunctionality #$i ()
  
  v:T @lvl, w:P[v/x1] @lvl, J ⊢ Q[v/x2] ext t
  v:T @lvl, w:P ∈ 𝕌{lvl}[v/x1], J ⊢ Q ∈ 𝕌{lvl}[v/x2]

Rule: inlEquality
This rule proved as lemma rule_inl_equality_true in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (inl a1) (inl a2) ∈ (A B)

  BY inlEquality !parameter{i:l} ()
  
  H  ⊢ a1 a2 ∈ A
  H  ⊢ B ∈ Type

Rule: impliesLevelFunctionality
x:(P  Q ∈ 𝕌{lvl}), J ⊢  B ∈ 𝕌{lvl} ext experimental{impliesLevelFunctionality}(Ax)

  BY impliesLevelFunctionality #$i ()
  
  v:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}
  v:A, w:(Q ∈ 𝕌{lvl}), J ⊢ B ∈ 𝕌{lvl}
  v:(P ∈ 𝕌{lvl}), w:A @lvl, J ⊢ P

Rule: allLevelFunctionality
x:(∀x1:T. P ∈ 𝕌{lvl}), J ⊢ ∀x2:T. Q ∈ 𝕌{lvl} ext experimental{allLevelFunctionality}(λx.Ax)

  BY allLevelFunctionality #$i ()
  
  v:T @lvl, w:P ∈ 𝕌{lvl}[v/x1], J ⊢ Q ∈ 𝕌{lvl}[v/x2]

Rule: allFunctionality
f:(∀x1:T. P) @lvl, J ⊢ ∀x2:T. ext experimental{allFunctionality}(λv.!((!\\w.t) v))

  BY allFunctionality #$i ()
  
  v:T @lvl, w:P[v/x1] @lvl, J ⊢ Q[v/x2] ext t

Rule: isectEquality
This rule proved as lemma rule_isect_equality_true3 in file rules/rules_isect.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (⋂x1:a1. b1) (⋂x2:a2. b2) ∈ Type

  BY isectEquality ()
  
  H  ⊢ a1 a2 ∈ Type
  y:a1 ⊢ b1[y/x1] b2[y/x2] ∈ Type

Rule: orFunctionality
x:(P ∨ Q) @lvl, J ⊢ A ∨ ext experimental{orFunctionality}(case of inl(v) => inl inr(v) => inr )

  BY orFunctionality #$i ()
  
  v:P @lvl, J ⊢ ext a
  v:Q @lvl, J ⊢ ext b
  v:(Q ∈ 𝕌{lvl}), w:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}
  v:(P ∈ 𝕌{lvl}), w:(Q ∈ 𝕌{lvl}), J ⊢ B ∈ 𝕌{lvl}

Rule: impliesFunctionality
f:(P  Q) @lvl, J ⊢  ext experimental{impliesFunctionality}(λa.!((!\\w.h) g))

  BY impliesFunctionality #$i ()
  
  a:A @lvl, J ⊢ ext g
  a:A @lvl, w:Q @lvl, J ⊢ ext h
  a:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}

Rule: equalityUniverse
This rule proved as lemma rule_equality_universe_true3 in file rules/rules_equality6.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ A1 A2 ∈ Type

  BY equalityUniverse x1 y1 x2 y2 ()
  
  H  ⊢ (x1 y1 ∈ A1) (x2 y2 ∈ A2) ∈ Type

Rule: divideEquality
This rule proved as lemma rule_arithop_equality_true3 in file rules/rules_arith.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (m1 ÷ n1) (m2 ÷ n2) ∈ ℤ

  BY divideEquality ()
  
  H  ⊢ m1 m2 ∈ ℤ
  H  ⊢ n1 n2 ∈ ℤ
  H  ⊢ n1 ≠ 0

Rule: comment
H  ⊢ ext .T) c

  BY comment ()
  
  H  ⊢ ext T

Rule: equalityElimination
x:(p q ∈ A), J ⊢ ext t

  BY equalityElimination #$i
  
  x:(p q ∈ A), J[Ax/x] ⊢ C[Ax/x] ext t

Rule: addEquality
This rule proved as lemma rule_arithop_equality_true3 in file rules/rules_arith.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (m1 n1) (m2 n2) ∈ ℤ

  BY addEquality ()
  
  H  ⊢ m1 m2 ∈ ℤ
  H  ⊢ n1 n2 ∈ ℤ

Rule: hypothesis_subsumption
x:A, J ⊢ ext t

  BY hypothesis_subsumption #$i ()
  
  H  ⊢ B ⊆A
  x:A, J ⊢ x ∈ B
  x:B, J ⊢ ext t

Rule: computeAll
H  ⊢ b

  BY computeAll ()
     
     CallLisp(COMPUTE-ALL)
  No Subgoals

Rule: int_eqEquality
H  ⊢ if a1=b1  then s1  else t1 if a2=b2  then s2  else t2 ∈ T

  BY int_eqEquality v
  
  H  ⊢ a1 a2 ∈ ℤ
  H  ⊢ b1 b2 ∈ ℤ
  v:(a1 b1 ∈ ℤ) ⊢ s1 s2 ∈ T
  v:((a1 b1 ∈ ℤ) ⟶ Void) ⊢ t1 t2 ∈ T

Rule: intWeakElimination
x:ℤJ ⊢ b ∈ T

  BY intWeakElimination #$i v
  
  x:ℤJ, y:ℤv:y < 0, z:a b ∈ T[y 1/x] ⊢ b ∈ T[y/x]
  x:ℤJ ⊢ b ∈ T[0/x]
  x:ℤJ, y:ℤv:0 < y, z:a b ∈ T[y 1/x] ⊢ b ∈ T[y/x]

Rule: isect_memberFormation
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ⋂x:A. ext b

  BY isect_memberFormation !parameter{i:l} ()
  
  [z:A] ⊢ B[z/x] ext b
  H  ⊢ A ∈ Type

Rule: lemma_by_obid
H  ⊢ ext t

  BY lemma_by_obid !parameter{$theorem:o} ()
     
     Let CallLisp(LE-LEMMA-O)
  No Subgoals

Rule: dependent_pairFormation
This rule proved as lemma rule_pair_formation_true in file rules/rules_product.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ x:A × ext <a, b>

  BY dependent_pairFormation !parameter{i:l} ()
  
  H  ⊢ a ∈ A
  H  ⊢ B[a/x] ext b
  y:A ⊢ B[y/x] B[y/x] ∈ Type

Rule: exceptionSqequal
This rule proved as lemma rule_exception_sqequal_true in file rules/rules_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ext c

  BY exceptionSqequal ()
  
  H  ⊢ is-exception(t)
  [u:Base], [v:Base], [x:(t exception(u; v))] ⊢ ext c
  u:Base, v:Base ⊢ t ∈ Base

Rule: decideExceptionCases
This rule proved as lemma rule_decide_exception_cases_true in file rules/rules_decide_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY decideExceptionCases y.u z.v ()
  
  H  ⊢ is-exception(case of inl(y) => inr(z) => v)
  x:(t ∈ Top Top) ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Rule: closedConclusion
This rule proved as lemma rule_closed_conclusion_true3 in file rules/rules_struct2.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ext t

  BY closedConclusion ()
  
     ⊢ ext t

Rule: baseApply
This rule proved as lemma rule_apply_in_base_true3 in file rules/rules_squiggle6.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ a ∈ Base

  BY baseApply ()
  
  H  ⊢ f ∈ Base
  H  ⊢ a ∈ Base

Rule: sqleReflexivity
This rule proved as lemma rule_approx_refl_true3 in file rules/rules_squiggle.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ a ≤ a

  BY sqleReflexivity ()
  
  No Subgoals

Rule: unionElimination
This rule proved as lemma rule_union_elimination_true in file rules/rules_union.v
 at https://github.com/vrahli/NuprlInCoq  

z:(A B) @lvl, J ⊢ ext case of inl(x) => left inr(y) => right

  BY unionElimination #$i y
  
  z:(A B), x:A @lvl, J[inl x/z] ⊢ T[inl x/z] ext left
  z:(A B), y:B @lvl, J[inr /z] ⊢ T[inr /z] ext right

Rule: unionEquality
This rule proved as lemma rule_union_equality_true in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (a1 b1) (a2 b2) ∈ Type

  BY unionEquality ()
  
  H  ⊢ a1 a2 ∈ Type
  H  ⊢ b1 b2 ∈ Type

Rule: callbyvalueDecide
This rule proved as lemma rule_halt_decide_true3 in file rules/rules_halts_decide.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ d ∈ Top Top

  BY callbyvalueDecide y.a z.b ()
  
  H  ⊢ 0 ≤ eval case of inl(y) => inr(z) => b; 0
  H  ⊢ d ∈ Base

Rule: promote_hyp
x:A @lvl1, J, y:B @lvl2, K ⊢ ext t

  BY promote_hyp #$i #$j ()
  
  y:B @lvl2, x:A @lvl1, J, K ⊢ ext t

Rule: levelHypothesis
x:A @i, J ⊢ A ∈ Type

  BY levelHypothesis #$h
  
  No Subgoals

Rule: imageElimination
This rule proved as lemma rule_image_elimination_true in file rules/rules_image.v
 at https://github.com/vrahli/NuprlInCoq  

x:Image(A,f) @lvl, J ⊢ ext t

  BY imageElimination #$i ()
  
  [w:A] @lvl, J[f w/x] ⊢ C[f w/x] ext t

Rule: applyLambdaEquality
  This rule combines the rules Error :applyEquality and Error :lambdaEquality
but generates one fewer subgoal because the subgoal H  ⊢ A  generated
by `lambdaEquality` is not needed because the subgoal H  ⊢ a1 a2
generated by `applyEquality` also implies that is type.


H  ⊢ ((λx1.b1) a1) ((λx2.b2) a2) ∈ B[a1/x]

  BY applyLambdaEquality (x:A ⟶ B) ()
  
  z:A ⊢ b1[z/x1] b2[z/x2] ∈ B[z/x]
  H  ⊢ a1 a2 ∈ A

Rule: hyp_replacement
This rule proved as lemma rule_hyp_replacement_true3 in file rules_equality7.v at https://github.com/vrahli/NuprlInCoq  

This is the rule that states that types are extensional.
If is provably equal to in ⌜Type⌝ then we can replace hypothesis x:A
by hypothesis x:B.
In particular,  from x:B we have ⌜x ∈ B⌝ and therefore ⌜x ∈ A⌝.⋅

x:A, J ⊢ ext t

  BY hyp_replacement #$j !parameter{i:l} ()
  
  x:B, J ⊢ ext t
  x:A, J ⊢ B ∈ Type

Rule: inlFormation
This rule proved as lemma rule_inr_formation_true3 in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ext inl a

  BY inlFormation !parameter{i:l} ()
  
  H  ⊢ ext a
  H  ⊢ B ∈ Type

Rule: inrFormation
This rule proved as lemma rule_inr_formation_true3 in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ext inr 

  BY inrFormation !parameter{i:l} ()
  
  H  ⊢ ext b
  H  ⊢ A ∈ Type

Rule: addLevel
x:A, J ⊢ ext t

  BY addLevel !parameter{lvl:l} #$h ()
  
  x:A @lvl, J ⊢ ext t
  x:A, J ⊢ A ∈ 𝕌{lvl}

Rule: functionExtensionality
H  ⊢ g ∈ (x:A ⟶ B) ext t

  BY functionExtensionality !parameter{i:l} ()
  
  u:A ⊢ (f u) (g u) ∈ B[u/x] ext t
  H  ⊢ A ∈ Type

Rule: functionEquality
This rule proved as lemma rule_function_equality_true in file rules/rules_function.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (x1:a1 ⟶ b1) (x2:a2 ⟶ b2) ∈ Type

  BY functionEquality y
  
  H  ⊢ a1 a2 ∈ Type
  y:a1 ⊢ b1[y/x1] b2[y/x2] ∈ Type

Rule: voidEquality
This rule proved as lemma rule_void_equality_true3 in file rules/rules_void.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ Void Void ∈ Type

  BY voidEquality ()
  
  No Subgoals

Rule: voidElimination
This rule proved as lemma rule_void_elimination_true in file rules/rules_void.v
 at https://github.com/vrahli/NuprlInCoq  

z:Void, J ⊢ ext any z

  BY voidElimination #$i
  
  No Subgoals

Rule: isect_memberEquality
This rule proved as lemma rule_isect_member_equality_true in file rules/rules_isect2.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b1 b2 ∈ (⋂x:A. B)

  BY isect_memberEquality !parameter{i:l} ()
  
  z:A ⊢ b1 b2 ∈ B[z/x]
  H  ⊢ A ∈ Type

Rule: independent_pairEquality
H  ⊢ <a1, b1> = <a2, b2> ∈ (A × B)

  BY independent_pairEquality ()
  
  H  ⊢ a1 a2 ∈ A
  H  ⊢ b1 b2 ∈ B

Rule: axiomEquality
This rule proved as lemma rule_axiom_equality_true3 in file rules/rules_equality4.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ Ax Ax ∈ (a1 a2 ∈ A)

  BY axiomEquality ()
  
  H  ⊢ a1 a2 ∈ A

Rule: independent_isectElimination
f:(⋂x:A. B), J ⊢ ext !((!\\y.t) f)

  BY independent_isectElimination #$i ()
  
  f:(⋂x:A. B), J ⊢ A
  f:(⋂x:A. B), J, y:B ⊢ ext t

Rule: equalitySymmetry
This rule proved as lemma rule_equality_symmetry_true3 in file rules/rules_equality5.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ t ∈ T

  BY equalitySymmetry ()
  
  H  ⊢ s ∈ T

Rule: equalityTransitivity
This rule proved as lemma rule_equality_transitivity_true3 in file rules/rules_equality5.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ t ∈ T

  BY equalityTransitivity x
  
  H  ⊢ x ∈ T
  H  ⊢ t ∈ T

Rule: intEquality
This rule proved as lemma rule_int_equality_true3 in file rules/rules_number.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ℤ = ℤ ∈ Type

  BY intEquality ()
  
  No Subgoals

Rule: productEquality
This rule proved as lemma rule_product_equality_true in file rules/rules_product.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (x1:a1 × b1) (x2:a2 × b2) ∈ Type

  BY productEquality y
  
  H  ⊢ a1 a2 ∈ Type
  y:a1 ⊢ b1[y/x1] b2[y/x2] ∈ Type

Rule: baseClosed
This rule proved as lemma rule_base_closed_true in file rules/rules_base.v at https://github.com/vrahli/NuprlInCoq  

   ⊢ t ∈ Base

  BY baseClosed ()
  
  No Subgoals

Rule: imageMemberEquality
This rule proved as lemma rule_image_member_equality_true in file rules/rules_image.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (f a1) (f a2) ∈ Image(A,f)

  BY imageMemberEquality ()
  
  H  ⊢ a1 a2 ∈ A
  H  ⊢ f ∈ Base

Rule: tokenEquality
H  ⊢ "$tok" "$tok" ∈ Atom

  BY tokenEquality ()
  
  No Subgoals

Rule: atomEquality
H  ⊢ Atom Atom ∈ Type

  BY atomEquality ()
  
  No Subgoals

Rule: equalityEquality
H  ⊢ (a11 a12 ∈ A1) (a21 a22 ∈ A2) ∈ Type

  BY equalityEquality ()
  
  H  ⊢ A1 A2 ∈ Type
  H  ⊢ a11 a21 ∈ A1
  H  ⊢ a12 a22 ∈ A1

Rule: independent_pairFormation
H  ⊢ A × ext <a, b>

  BY independent_pairFormation ()
  
  H  ⊢ ext a
  H  ⊢ ext b

Rule: independent_functionElimination
f:F @lvl, J ⊢ ext !((!\\y.t) a)

  BY independent_functionElimination #$i y
     
     Let A ⟶ F
  f:F, J ⊢ ext a
  f:F, J, y:B @lvl ⊢ ext t

Rule: setEquality
This rule proved as lemma rule_set_equality_true in file rules/rules_set.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ {x1:A1| B1}  {x2:A2| B2}  ∈ Type

  BY setEquality x
  
  H  ⊢ A1 A2 ∈ Type
  x:A1 ⊢ B1[x/x1] B2[x/x2] ∈ Type

Rule: dependent_set_memberEquality
H  ⊢ a1 a2 ∈ {x:A| B} 

  BY dependent_set_memberEquality !parameter{i:l} ()
  
  H  ⊢ a1 a2 ∈ A
  H  ⊢ B[a1/x]
  y:A ⊢ B[y/x] B[y/x] ∈ Type

Rule: because_Cache
H  ⊢ C

  BY because_Cache ()
  
  No Subgoals

Rule: hypothesisEquality
This rule proved as lemma rule_hypothesis_equality_true in file rules/rules_struct.v
 at https://github.com/vrahli/NuprlInCoq  

x:T, J ⊢ x ∈ T

  BY hypothesisEquality #$i
  
  No Subgoals

Rule: applyEquality
This rule proved as lemma rule_apply_equality_true in file rules/rules_function.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ (f1 a1) (f2 a2) ∈ B[a1/x]

  BY applyEquality x:A ⟶ B
  
  H  ⊢ f1 f2 ∈ (x:A ⟶ B)
  H  ⊢ a1 a2 ∈ A

Rule: universeEquality
This rule proved as lemma rule_universe_equality_true3 in file rules/rules_uni.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ 𝕌{j} = 𝕌{j} ∈ Type

  BY universeEquality ()
     
     CallLisp(LE-UNIVERSE-EQUALITY)
  No Subgoals

Rule: lambdaEquality
This rule proved as lemma rule_lambda_equality_true in file rules/rules_function.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ x1.b1) x2.b2) ∈ (x:A ⟶ B)

  BY lambdaEquality !parameter{i:l} ()
  
  z:A @i ⊢ b1[z/x1] b2[z/x2] ∈ B[z/x]
  H  ⊢ A ∈ Type

Rule: sqequalRule
H  ⊢ ext t

  BY sqequal ()
     
     Let SubGoals CallLisp(SQEQ)
  SubGoals

Rule: dependent_functionElimination
f:(x:A ⟶ B) @lvl, J ⊢ ext !((!\y,v.t) Ax)

  BY dependent_functionElimination #$i v
  
  f:(x:A ⟶ B), J ⊢ a ∈ A
  f:(x:A ⟶ B), J, y:B[a/x] @lvl, v:(y (f a) ∈ B[a/x]) ⊢ ext t

Rule: cumulativity
This rule proved as lemma rule_cumulativity_true3 in file rules/rules_uni.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ t ∈ Type

  BY cumulativity !parameter{j:l} ()
     
     CallLisp(LE_CUMULATIVITY)
  H  ⊢ t ∈ 𝕌{j}

Rule: instantiate
!subst(J; subs) ⊢ !subst(C; subs) ext !subst(t; subs)

  BY instantiate subs ()
  
  J  ⊢ ext t

Rule: hypothesis
This rule proved as lemma rule_hypothesis_true3 in file rules/rules_struct.v at https://github.com/vrahli/NuprlInCoq  

x:A, J ⊢ ext x

  BY hypothesis #$i
  
  No Subgoals

Rule: natural_numberEquality
This rule proved as lemma rule_natural_number_equality_true3 in file rules/rules_number.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ $i $i ∈ ℤ

  BY natural_numberEquality ()
  
  No Subgoals

Rule: isectElimination
f:(⋂x:A. B), J ⊢ ext !((!\y,v.t) Ax)

  BY isectElimination #$i ()
  
  f:(⋂x:A. B), J ⊢ a ∈ A
  f:(⋂x:A. B), J, y:B[a/x], v:(y f ∈ B[a/x]) ⊢ ext t

Rule: extract_by_obid
H  ⊢ t ∈ C

  BY extract_by_obid !parameter{$theorem:o} ()
     
     Let CallLisp(LE-LEMMA-O)
  No Subgoals

Rule: introduction
This rule proved as lemma rule_introduction_true3 in file rules/rules_struct.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ext t

  BY introduction t
  
  H  ⊢ t ∈ T

Rule: productElimination
This rule proved as lemma rule_product_elimination_true in file rules/rules_product.v
 at https://github.com/vrahli/NuprlInCoq  

z:(x:A × B) @lvl, J ⊢ ext let u,v in t

  BY productElimination #$i v
  
  z:(x:A × B), u:A @lvl, v:B[u/x] @lvl, J[<u, v>/z] ⊢ T[<u, v>/z] ext t

Rule: rename
y:a @lvl, J ⊢ ext !((!\\x.T) y)

  BY rename #$i ()
  
  x:a @lvl, J[x/y] ⊢ C[x/y] ext T

Rule: thin
This rule proved as lemma rule_thin_true in file rules/rules_struct.v at https://github.com/vrahli/NuprlInCoq  

x:A, J ⊢ ext t

  BY thin #$i
  
  J ⊢ ext t

Rule: setElimination
This rule proved as lemma rule_set_elimination_true in file rules/rules_set.v at https://github.com/vrahli/NuprlInCoq  

u:{x:A| B}  @lvl, J ⊢ ext !((!\\y.t) u)

  BY setElimination #$i v
  
  u:{x:A| B} y:A @lvl, [v:B[y/x]] @lvl, J[y/u] ⊢ T[y/u] ext t

Rule: sqequalHypSubstitution
This rule proved as lemma rule_cequiv_subst_hyp_true in file rules/rules_squiggle2.v
 at https://github.com/vrahli/NuprlInCoq  

j:T[a/x] @lvl, J ⊢ ext t

  BY sqequalHypSubstitution #$i (a b) x.T ()
  
  j:T[a/x] @lvl, J ⊢ b
  j:T[b/x] @lvl, J ⊢ ext t

Rule: cut
This rule proved as lemma rule_cut_true3 in file rules/rules_struct.v at https://github.com/vrahli/NuprlInCoq  

J ⊢ ext x.t) s

  BY cut #$i x
  
  J ⊢ ext s
  x:S, J ⊢ ext t

Rule: lambdaFormation
This rule proved as lemma rule_lambda_formation_true in file rules/rules_function.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ x:A ⟶ ext λz.b

  BY lambdaFormation !parameter{i:l} ()
  
  z:A @i ⊢ B[z/x] ext b
  H  ⊢ A ∈ Type

Rule: sqequalReflexivity
This rule proved as lemma rule_cequiv_refl_true in file rules/rules_squiggle.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ a

  BY sqequalReflexivity ()
  
  No Subgoals

Rule: computationStep
H  ⊢ b

  BY computationStep ()
     
     CallLisp(COMPUTATION-STEP)
  No Subgoals

Rule: sqequalTransitivity
This rule proved as lemma rule_cequiv_trans_true3 in file rules/rules_squiggle8.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b

  BY sqequalTransitivity c
  
  H  ⊢ c
  H  ⊢ b

Rule: sqequalSubstitution
This rule proved as lemma rule_cequiv_subst_concl_true3 in file rules/rules_squiggle2.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ T[a/x] ext t

  BY sqequalSubstitution (a b) x.T ()
  
  H  ⊢ b
  H  ⊢ T[b/x] ext t



Home Index