Proof step 41 from proof subst-KK-equal (conclusion)

User applied rule structural induction

And obtained the following new goals

• Proof step 14:

  O[K _ v1 _ v2] = C0[K _ v _ v0], value(v1), value(v2), value(v), value(v0), context(C0), context(O) ⊦ O[v1] = C0[v]

• Proof step 30:

  ∀ v1, v2, C0, v, v0. C1[K _ v1 _ v2] = C0[K _ v _ v0] ∧ value(v1) ∧ value(v2) ∧ value(v) ∧ value(v0) ∧ context(C0) ∧ context(C1) → C1[v1] = C0[v], (C1 _ t)[K _ v1 _ v2] = C0[K _ v _ v0], value(v1), value(v2), value(v), value(v0), context(C0), context(C1 _ t) ⊦ (C1 _ t)[v1] = C0[v]

• Proof step 40:

  ∀ v1, v2, C0, v, v0. C1[K _ v1 _ v2] = C0[K _ v _ v0] ∧ value(v1) ∧ value(v2) ∧ value(v) ∧ value(v0) ∧ context(C0) ∧ context(C1) → C1[v1] = C0[v], (t _ C1)[K _ v1 _ v2] = C0[K _ v _ v0], value(v1), value(v2), value(v), value(v0), context(C0), context(t _ C1) ⊦ (t _ C1)[v1] = C0[v]

Rule argument

Additional information

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