Step * of Lemma atom-sdata-one-one

[a,b:Atom1].  uiff(data(a) data(b) ∈ SecurityData;a b ∈ Atom1)
BY
Auto }

1
1. Atom1
2. Atom1
3. data(a) data(b) ∈ SecurityData
⊢ b ∈ Atom1


Latex:



Latex:
\mforall{}[a,b:Atom1].    uiff(data(a)  =  data(b);a  =  b)


By


Latex:
Auto




Home Index