---

Step * of Lemma agree_on_common_wf

∀[T:Type]. ∀[as,bs:T List].  (agree_on_common(T;as;bs) ∈ ℙ)
BY
{ (((((InductionOnList THEN InductionOnList) THEN RecUnfold `agree_on_common` 0) THEN Reduce 0) THEN Auto{1,3}-1)
   THEN EasyHyp
   ) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:T  List].    (agree\_on\_common(T;as;bs)  \mmember{}  \mBbbP{})


By

---

Latex:
(((((InductionOnList  THEN  InductionOnList)  THEN  RecUnfold  `agree\_on\_common`  0)  THEN  Reduce  0)
    THEN  Auto\{1,3\}-1
    )
  THEN  EasyHyp
  )

---

Home Index