proposition: Remark R4_3_3: const_pathS_eps n2 alpha (canon beta (S n1)).
proof: Proof. eapply const_pathS_eps_trans with beta; auto. - apply R4_3_1 . - apply R4_3_2. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)