proposition: Lemma demo_arrow_1 : forall a b, P1 a -> P2 b -> forall c d, P3 c -> P1 d -> c = b.
proof: Proof. Proof using. dup 4. =>>. =>>. demo. =>> A. =>> B. =>>. =>> C D. demo. =>> A B. =>>. demo. =>> A B. =>>. =>> C D. demo. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia