(* Main properties **********************************************************)
theorem ceq_ext_trans: ∀L1,I1,I. ceq_ext L1 I1 I →
(* Main properties **********************************************************)
theorem ceq_ext_trans: ∀L1,I1,I. ceq_ext L1 I1 I →