proposition: Lemma le8_trans T0 T1 T2 T3 T4 T5 T6 T7(r0 r1 r2 : rel8 T0 T1 T2 T3 T4 T5 T6 T7) (LE0 : r0 <8== r1) (LE1 : r1 <8== r2) : r0 <8== r2.
proof: Proof. do 8 intro. intros H. eapply LE1, LE0, H. Qed.
imports: Paco(paconotation)