DEFINITION insert_eq()
TYPE =
       ∀S:Set
         .∀x:S
           .∀P:S→Prop
             .∀G:S→Prop
               .(∀y:S.(P y)→(eq S y x)→(G y))→(P x)→(G x)
BODY =
Show proof