Step * of Lemma cbv-all-identity

[T:Type]. ∀[t:T].  let x ⟵ in x ∈ supposing valueall-type(T)
BY
Auto }


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}[t:T].    let  x  \mleftarrow{}{}  t  in  x  \mmember{}  T  supposing  valueall-type(T)


By


Latex:
Auto




Home Index