proposition: Theorem seq_cons : forall n1 n2 s1 s2 (SEQ : seq (cons n1 s1) (cons n2 s2)), n1 = n2 /\ seq s1 s2.
proof: Proof. intros. inversion_clear SEQ; rename H into SEQ. inversion_clear SEQ; auto. Qed.
imports: Setoid Program Paco.paco