proposition: Lemma snoc_inj : forall T, forall l1 l2 : list T, forall x1 x2 : T, snoc l1 x1 = snoc l2 x2 -> l1 = l2 # x1 = x2.
proof: Proof. induction l1; simpl; intros. destruct l2; simpl in H; inversion H; subst; auto. inversion H. destruct l2; simpl in H1; inversion H1. destruct l2; simpl in H. inversion H. destruct l1; simpl in H2; inversion H2. inversion H. apply IHl1 in H2. sp; subst; auto. Qed.
imports: UsefulTypes bin_rels Omega