---

Step * of Lemma agree_on_common_weakening

∀[T:Type]. ∀as,bs:T List.  agree_on_common(T;as;bs) supposing as = bs ∈ (T List)
BY
{ ((Auto THEN HypSubst' (-1) 0)
   THEN ThinVar `as'
   THEN ListInd 2
   THEN RecUnfold `agree_on_common` 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  HypSubst'  (-1)  0)
  THEN  ThinVar  `as'
  THEN  ListInd  2
  THEN  RecUnfold  `agree\_on\_common`  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index