 Persistence of intuitionistic Kripke forcing

ID: persistence-of-intuitionistic-kripke-forcing

w \leq v

and

w ⊩ A

, then

v ⊩ A

. The proof is by structural induction on

A

 New to topics? Read the docs here!