### Nuprl Lemma : int_term_ind_wf_simple

`∀[A:Type]. ∀[v:int_term()]. ∀[Constant,Var:var:ℤ ⟶ A]. ∀[Add,Subtract,Multiply:left:int_term()`
`                                                                                ⟶ right:int_term()`
`                                                                                ⟶ A`
`                                                                                ⟶ A`
`                                                                                ⟶ A].`
`∀[Minus:num:int_term() ⟶ A ⟶ A].`
`  (int_term_ind(v;`
`                itermConstant(const)`` Constant[const];`
`                itermVar(var)`` Var[var];`
`                itermAdd(left,right)`` rec1,rec2.Add[left;right;rec1;rec2];`
`                itermSubtract(left,right)`` rec3,rec4.Subtract[left;right;rec3;rec4];`
`                itermMultiply(left,right)`` rec5,rec6.Multiply[left;right;rec5;rec6];`
`                itermMinus(num)`` rec7.Minus[num;rec7])  ∈ A)`

Proof

Definitions occuring in Statement :  int_term_ind: int_term_ind int_term: `int_term()` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2;s3;s4]` so_apply: `x[s1;s2]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` int: `ℤ` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` true: `True` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` all: `∀x:A. B[x]`
Lemmas referenced :  int_term_ind_wf true_wf int_term_wf subtype_rel_dep_function istype-int istype-universe
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule Error :lambdaEquality_alt,  Error :universeIsType,  functionExtensionality applyEquality Error :dependent_set_memberEquality_alt,  natural_numberEquality Error :inhabitedIsType,  equalityTransitivity equalitySymmetry closedConclusion intEquality functionEquality because_Cache setEquality independent_isectElimination Error :lambdaFormation_alt,  Error :setIsType,  setElimination rename applyLambdaEquality Error :functionIsType,  instantiate universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[v:int\_term()].  \mforall{}[Constant,Var:var:\mBbbZ{}  {}\mrightarrow{}  A].  \mforall{}[Add,Subtract,Multiply:left:int\_term()
{}\mrightarrow{}  right:int\_term()
{}\mrightarrow{}  A
{}\mrightarrow{}  A
{}\mrightarrow{}  A].
\mforall{}[Minus:num:int\_term()  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
(int\_term\_ind(v;
itermConstant(const){}\mRightarrow{}  Constant[const];
itermVar(var){}\mRightarrow{}  Var[var];