Cwm/log/n3 rfe: subst

Found this while reviewing notes on my WearableGizmo; composed it while 
jetlagged in Japan diring the TAG meeting...

( 'fido 'X {X a Dog}) subst { fido a Dog }.

C setofall ('X {X a Int. X < 3 }).

{ C setofall (V F) } <=> { this log:forall X. { X a C } <=> (X V 
F).subst }.

Hmmm... Would this work for induction?
--
Dan Connolly, W3C http://www.w3.org/People/Connolly/