Proof

Definitions occuring in Statement :  radd-list: radd-list(L) real: list: List uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T radd-list: radd-list(L) callbyvalueall: callbyvalueall uimplies: supposing a has-value: (a)↓ has-valueall: has-valueall(a) nat: so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False nat_plus: + ge: i ≥  nequal: a ≠ b ∈  decidable: Dec(P) le: A ≤ B satisfiable_int_formula: satisfiable_int_formula(fmla) not: ¬A top: Top
Lemmas referenced :  real-list-has-valueall evalall-reduce list_wf real_wf valueall-type-real-list value-type-has-value nat_wf set-value-type le_wf int-value-type length_wf_nat eq_int_wf length_wf bool_wf eqtt_to_assert assert_of_eq_int int-to-real_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int accelerate_wf non_neg_length decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf intformle_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_eq_lemma int_formula_prop_wf less_than_wf reg-seq-list-add_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis callbyvalueReduce independent_isectElimination intEquality lambdaEquality natural_numberEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination because_Cache voidElimination dependent_set_memberEquality int_eqEquality isect_memberEquality voidEquality independent_pairFormation computeAll axiomEquality

Latex: