proposition: Lemma demo_arrow_3 : forall (a:nat), a = 0%nat -> Sym a.
proof: Proof. Proof using. dup 5. =>>. demo. =>> E. demo. =>> E; =>> F. demo. =>> E; =>> F G. demo. try (=>> E; =>> F G H). demo. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia