---

Step * of Lemma test36

λz,loc,L. if (∃l∈L.IdDeq l loc)_b then {L} else {[loc / L]} fi  ∈ ∩A:Type. (A ─→ Id ─→ (Id List) ─→ bag(Id List))
BY
{ (UseSimpleTypeInf THEN CongruenceAuto) }

---

Latex:


\mlambda{}z,loc,L.  if  (\mexists{}l\mmember{}L.IdDeq  l  loc)\_b  then  \{L\}  else  \{[loc  /  L]\}  fi    \mmember{}  \mcap{}A:Type
                                                                                                                        (A  {}\mrightarrow{}  Id  {}\mrightarrow{}  (Id  List)  {}\mrightarrow{}  bag(Id  List))


By

(UseSimpleTypeInf  THEN  CongruenceAuto)

---

Home Index