DEFINITION csubt_pc3()
TYPE =
       ∀g:G.∀c1:C.∀t1:T.∀t2:T.(pc3 c1 t1 t2)→∀c2:C.(csubt g c1 c2)→(pc3 c2 t1 t2)
BODY =
        assume g: G
        assume c1: C
        assume t1: T
        assume t2: T
        suppose H: pc3 c1 t1 t2
          (h1) 
              assume t: T
              assume c2: C
              suppose : csubt g c1 c2
                by (pc3_refl . .)
                we proved pc3 c2 t t
∀t:T.∀c2:C.(csubt g c1 c2)→(pc3 c2 t t)
          end of h1
          (h2) 
              assume t0: T
              assume t3: T
              suppose H0: pr2 c1 t0 t3
              assume t4: T
              suppose : pc3 c1 t3 t4
              suppose H2: ∀c2:C.(csubt g c1 c2)→(pc3 c2 t3 t4)
              assume c2: C
              suppose H3: csubt g c1 c2
                (h1) 
                   by (csubt_pr2 . . . . H0 . H3)
                   we proved pr2 c2 t0 t3
                   by (pc3_pr2_r . . . previous)
pc3 c2 t0 t3
                end of h1
                (h2) by (H2 . H3) we proved pc3 c2 t3 t4
                by (pc3_t . . . h1 . h2)
                we proved pc3 c2 t0 t4

                ∀t0:T
                  .∀t3:T
                    .pr2 c1 t0 t3
                      →∀t4:T.(pc3 c1 t3 t4)→(∀c2:C.(csubt g c1 c2)→(pc3 c2 t3 t4))→∀c2:C.(csubt g c1 c2)→(pc3 c2 t0 t4)
          end of h2
          (h3) 
              assume t0: T
              assume t3: T
              suppose H0: pr2 c1 t0 t3
              assume t4: T
              suppose : pc3 c1 t0 t4
              suppose H2: ∀c2:C.(csubt g c1 c2)→(pc3 c2 t0 t4)
              assume c2: C
              suppose H3: csubt g c1 c2
                (h1) 
                   by (csubt_pr2 . . . . H0 . H3)
                   we proved pr2 c2 t0 t3
                   by (pc3_pr2_x . . . previous)
pc3 c2 t3 t0
                end of h1
                (h2) by (H2 . H3) we proved pc3 c2 t0 t4
                by (pc3_t . . . h1 . h2)
                we proved pc3 c2 t3 t4

                ∀t0:T
                  .∀t3:T
                    .pr2 c1 t0 t3
                      →∀t4:T.(pc3 c1 t0 t4)→(∀c2:C.(csubt g c1 c2)→(pc3 c2 t0 t4))→∀c2:C.(csubt g c1 c2)→(pc3 c2 t3 t4)
          end of h3
          by (pc3_ind_left . . h1 h2 h3 . . H)
          we proved ∀c2:C.(csubt g c1 c2)→(pc3 c2 t1 t2)
       we proved ∀g:G.∀c1:C.∀t1:T.∀t2:T.(pc3 c1 t1 t2)→∀c2:C.(csubt g c1 c2)→(pc3 c2 t1 t2)