Packages

o

provingground.library

LocalConstImpliesConstSym

object LocalConstImpliesConstSym

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. LocalConstImpliesConstSym
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Value Members

  1. val A: Typ[Term]
  2. val ass: FuncLike[RepTerm[SafeLong], Equality[Term]]
  3. val base: Refl[Term]
  4. val claim: Func[RepTerm[SafeLong], IdentityTyp[Term]]
  5. val f: Func[RepTerm[SafeLong], Term]
  6. val hyp: Equality[Term]
  7. val inductor: Func[Equality[Term], Func[FuncLike[Nat, Func[Equality[Term], Equality[Term]]], FuncLike[Nat, Equality[Term]]]]
  8. val pf: FuncLike[RepTerm[SafeLong], Equality[Term]]
  9. val step: Func[Equality[Term], Equality[Term]]
  10. val thm: GenFuncTyp[RepTerm[SafeLong], Equality[Term]]