Propositional formulation of ll equiv.
Some more progress on proof. Definition of SSNI.