---

Step * 1 1 2 of Lemma fset-max_wf

.....antecedent..... 
1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. f : T ⟶ ℕ
4. s : Base
5. s1 : Base
6. s = s1 ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
7. s ∈ T List
8. s1 ∈ T List
9. set-equal(T;s;s1)
10. eq : EqDecider(T)
⊢ Assoc(ℕ;λx,y. imax(x;y))
BY
{ ((D 0 THENA Auto) THEN (RepUR ``infix_ap`` 0 THEN Auto) THEN RW (AddrC [2] (LemmaC `imax_assoc`)) 0 THEN Auto)⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  f  :  T  {}\mrightarrow{}  \mBbbN{}
4.  s  :  Base
5.  s1  :  Base
6.  s  =  s1
7.  s  \mmember{}  T  List
8.  s1  \mmember{}  T  List
9.  set-equal(T;s;s1)
10.  eq  :  EqDecider(T)
\mvdash{}  Assoc(\mBbbN{};\mlambda{}x,y.  imax(x;y))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (RepUR  ``infix\_ap``  0  THEN  Auto)
  THEN  RW  (AddrC  [2]  (LemmaC  `imax\_assoc`))  0
  THEN  Auto)\mcdot{}

---

Home Index