#T elim T -T //
qed.
(* Basic eliminators ********************************************************)
axiom tw_wf_ind: ∀R:predicate term.
#T elim T -T //
qed.
(* Basic eliminators ********************************************************)
axiom tw_wf_ind: ∀R:predicate term.