proposition: Lemma snoc1 : forall T, forall a : list T, forall b x : T, snoc a b = [x] <=> a = [] # b = x.
proof: Proof. destruct a; simpl; sp; split; sp; subst; auto. inversion H; auto. inversion H; subst; auto. destruct a; simpl in H2; inversion H2. inversion H; subst; auto. destruct a; simpl in H2; inversion H2. Qed.
imports: UsefulTypes bin_rels Omega