Step * of Lemma has-valueall-if-has-value-callbyvalueall

[a,b:Base].  has-valueall(a) supposing (let x ⟵ in b[x])↓
BY
(Auto THEN UnfoldTopAb THEN UnfoldAtAddr [1] (-1) THEN HasValueD (-1) THEN Trivial) }


Latex:


Latex:
\mforall{}[a,b:Base].    has-valueall(a)  supposing  (let  x  \mleftarrow{}{}  a  in  b[x])\mdownarrow{}


By


Latex:
(Auto  THEN  UnfoldTopAb  0  THEN  UnfoldAtAddr  [1]  (-1)  THEN  HasValueD  (-1)  THEN  Trivial)




Home Index