Lemma ok_Bg_impl_ppermut:
forall G G' w C C',
okBg ((w, C) :: G) ->
G & (w, C) ~=~ G' & (w, C') ->
G ~=~ G' /\ C =_ C'.
Intuition:
We know that there is only one elem. with 1st = w, because otherwise okLF for worlds would fail.
This means that C =_ C', as they have the same unique 1st elem. of the pair.
Now, if that is the case and G & (w, C) ~=~ G' & (w, C') it follows that G ~=~ G'.
Ayertienna
commented
11 years ago
Lemma ok_Bg_impl_ppermut: forall G G' w C C', okBg ((w, C) :: G) -> G & (w, C) ~=~ G' & (w, C') -> G ~=~ G' /\ C =_ C'.
Intuition: We know that there is only one elem. with 1st = w, because otherwise okLF for worlds would fail. This means that C =_ C', as they have the same unique 1st elem. of the pair. Now, if that is the case and G & (w, C) ~=~ G' & (w, C') it follows that G ~=~ G'.