---

Step * 1 of Lemma word-rel-confluent


1. [X] : Type
⊢ rel-diamond-property((X + X) List;x,y.word-rel(X;x;y))
BY
{ (InstLemma `word-rel-diamond` [] THEN Fold `rel-diamond-property` (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  [X]  :  Type
\mvdash{}  rel-diamond-property((X  +  X)  List;x,y.word-rel(X;x;y))


By

---

Latex:
(InstLemma  `word-rel-diamond`  []  THEN  Fold  `rel-diamond-property`  (-1)  THEN  Auto)

---

Home Index