proposition: Lemma Sorted_snoc l x : Sorted R l → TlRel R x l → Sorted R (l ++ [x]).
proof: Proof. induction 1 as [|y l Hsort IH Hhd]; intros Htl; simpl. { repeat constructor. } constructor. - apply IH. inv Htl as [|? [|??]]; simplify_list_eq; by constructor. - destruct Hhd; constructor; [|done]. inv Htl as [|? [|??]]; by try discriminate_list. Qed.
imports: stdpp(options)