---

Step * of Lemma cons_interleaving2

∀[T:Type]. ∀x:T. ∀L,L1,L2:T List.  (interleaving(T;L1;L2;L) ⇒ interleaving(T;L1;[x / L2];[x / L]))
BY
{ ((((Auto THEN BackThruLemma `interleaving_symmetry`) THENM BackThruLemma `cons_interleaving`)
   THENM BackThruLemma `interleaving_symmetry`
   )
   THEN Auto
   ) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}L,L1,L2:T  List.    (interleaving(T;L1;L2;L)  {}\mRightarrow{}  interleaving(T;L1;[x  /  L2];[x  /  L]))


By

---

Latex:
((((Auto  THEN  BackThruLemma  `interleaving\_symmetry`)  THENM  BackThruLemma  `cons\_interleaving`)
  THENM  BackThruLemma  `interleaving\_symmetry`
  )
  THEN  Auto
  )

---

Home Index