Step * of Lemma has-value_wf_base

[a:Base]. ((a)↓ ∈ ℙ)
BY
(ProveWfLemma THEN Unfolds ``member prop`` THEN Refine `sqleIntensionalEquality` [] THEN Auto) }


Latex:


Latex:
\mforall{}[a:Base].  ((a)\mdownarrow{}  \mmember{}  \mBbbP{})


By


Latex:
(ProveWfLemma  THEN  Unfolds  ``member  prop``  0  THEN  Refine  `sqleIntensionalEquality`  []  THEN  Auto)




Home Index