Nuprl Lemma : ctt-eq

Nuprl Lemma : ctt-eq_wf

∀[a,b:CttTerm]. (ctt-eq{i:l}(a;b) ∈ ℙ')

Proof

Error : references

Latex:
\mforall{}[a,b:CttTerm]. (ctt-eq\{i:l\}(a;b) \mmember{} \mBbbP{}') Date html generated: 2020_05_21-AM-10_32_05 Last ObjectModification: 2020_05_13-PM-01_51_26 Theory : cubical!type!theory Home Index