INDUCTIVE DEFINITION wf3 () [ :G ]
OF ARITY C→C→Prop
BUILT FROM:
     wf3_sort: ∀m:nat.(wf3 g (CSort m) (CSort m))
   | wf3_bind: ∀c1:C
                       .∀c2:C
                         .wf3 g c1 c2
                           →∀u:T.∀t:T.(ty3 g c1 u t)→∀b:B.(wf3 g (CHead c1 (Bind b) u) (CHead c2 (Bind b) u))
   | wf3_void: ∀c1:C
                       .∀c2:C
                         .wf3 g c1 c2
                           →∀u:T
                                .∀t:T.(ty3 g c1 u t)→False
                                  →∀b:B.(wf3 g (CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort O)))
   | wf3_flat: ∀c1:C.∀c2:C.(wf3 g c1 c2)→∀u:T.∀f:F.(wf3 g (CHead c1 (Flat f) u) c2)