proposition: Lemma gt2_wf : WF gt2.
proof: Proof. apply WF_inverse. apply WF_inverse. apply wf_WF_transp. apply wf_lexprod. apply WF_wf_transp. apply gtC_wf. intro r. apply WF_wf_transp. apply wf_union_absorb. apply gt_args_lex_wf. class. apply WF_tc. apply gt0_wf. apply gt_red_wf. apply gt_args_lex_absorbs_gt_red. class. class. apply incl_tc. unfold gt0. rewrite restrict_union. fo. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)