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 =
        assume S: Set
        assume x: S
        assume P: S→Prop
        assume G: S→Prop
        suppose H: ∀y:S.(P y)→(eq S y x)→(G y)
        suppose H0: P x
          by (refl_equal . .)
          we proved eq S x x
          by (H . H0 previous)
          we proved G x
       we proved 
          ∀S:Set
            .∀x:S
              .∀P:S→Prop
                .∀G:S→Prop
                  .(∀y:S.(P y)→(eq S y x)→(G y))→(P x)→(G x)