proposition: Lemma seq_symm : forall s1 s2, seq s1 s2 -> seq s2 s1.
proof: Proof. pcofix CIH. intros s1 s2 H. pfold. punfold H. induction H; try constructor; auto. pclearbot. right. apply CIH. punfold R. Qed.
imports: ZArith List String Paco.paco