proposition: Lemma tail_of_decons : forall {A} {x : A} {l1 l2}, tail_of (cons x l1) l2 -> tail_of l1 l2.
proof: Proof. intros. remember (cons x l1) as l. revert Heql. revert l1. induction H; intros; subst; auto. Qed.
imports: Equations(Equations) Lia