Proof step 47 from proof subst-SK-equal (conclusion)

C[S _ v3 _ v4 _ v5] = C0[K _ v _ v0], value(v3), value(v4), value(v5), value(v), value(v0), context(C0), context(C) ⊦ C[v3 _ v5 _ (v4 _ v5)] = C0[v]

User applied rule structural induction

Proof step 20:
O[S _ v3 _ v4 _ v5] = C0[K _ v _ v0], value(v3), value(v4), value(v5), value(v), value(v0), context(C0), context(O) ⊦ O[v3 _ v5 _ (v4 _ v5)] = C0[v]
Proof step 36:
∀ v3, v4, v5, C0, v, v0. C1[S _ v3 _ v4 _ v5] = C0[K _ v _ v0] ∧ value(v3) ∧ value(v4) ∧ value(v5) ∧ value(v) ∧ value(v0) ∧ context(C0) ∧ context(C1) → C1[v3 _ v5 _ (v4 _ v5)] = C0[v], (C1 _ t)[S _ v3 _ v4 _ v5] = C0[K _ v _ v0], value(v3), value(v4), value(v5), value(v), value(v0), context(C0), context(C1 _ t) ⊦ (C1 _ t)[v3 _ v5 _ (v4 _ v5)] = C0[v]
Proof step 46:
∀ v3, v4, v5, C0, v, v0. C1[S _ v3 _ v4 _ v5] = C0[K _ v _ v0] ∧ value(v3) ∧ value(v4) ∧ value(v5) ∧ value(v) ∧ value(v0) ∧ context(C0) ∧ context(C1) → C1[v3 _ v5 _ (v4 _ v5)] = C0[v], (t _ C1)[S _ v3 _ v4 _ v5] = C0[K _ v _ v0], value(v3), value(v4), value(v5), value(v), value(v0), context(C0), context(t _ C1) ⊦ (t _ C1)[v3 _ v5 _ (v4 _ v5)] = C0[v]

[VARWITHVARSEQSARG : C, ()]

[[CONCRETESIMPRULES : ([CSIMPGEN : rawctxt generated by o, _, _;])]]