wf.art

notation syntax rels ;
import syntax wf ;

thm subclass-trans 
 if TE |- C0 subclass_of C1 a
    TE |- C1 subclass_of C2 
then TE |- C0 subclass_of C2
  proceed by rule induction on a with C0,C1 variable;
   case Refl; qed;
   case Step; qed by subclass_of__Step;
 end;

thm subinterface-trans 
 if TE |- C0 subinterface_of C1 a
    TE |- C1 subinterface_of C2 
then TE |- C0 subinterface_of C2
  proceed by rule induction on a with C0,C1 variable;
   case Refl; qed;
   case Step; qed by subinterface_of__Step;
 end;

thm wellfounded_interface-trans 
 if TE |- C0 subinterface_of C1 a
    TE |- C1 wellfounded_interface 
then TE |- C0 wellfounded_interface
  proceed by rule induction on a with C0,C1 variable;
   case Refl; qed by wellfounded_interface__Base;
   case Step; qed by wellfounded_interface__Step;
 end;