Weblog of Kenny

Lemma : Let R,p |- G and G |- \stripv(p) : R_G and R \cap \stript(p) \leq^u R_G and v \in [[R]] and (u v) = v' and flat(v) \in p => D and v' \in \stripv(p) =>^ML D' Then D(x) = flat(D(x)).