Beginner Question Thread

The atmosphere of /prog/ is not always welcoming to beginning programmers, so I hereby proactively create this thread as a safe place for beginning programmers. You may use this thread to discuss your experiences, feelings, and questions relating to your entering of the field of programming. Should you encounter any difficulty on your journey to becoming a computer scientist, have no fear, and post in here! However, try to keep the questions concept oriented, or on personal projects. It isn't enjoyable to do someone's homework for them. Special priority will be given to NEETs and those without access to an educational institution.

Hello /prog/, a Coq question (second exercise page 20 Coq in a hurry).

I'm trying to prove the following:
forall A B C D: Prop,(A->B)/\(C->D)/\A/\C -> B/\D
That is, in Coq, I have
Coq < Lemma example forall A B C D: Prop,(A->B)/\(C->D)/\A/\C -> B/\D.
1 subgoal
====
forall A B C D : Prop, (A->B)/\(C->D)/\A/\C -> B/\D
example < intros A B C D H.
1 subgoal

A : Prop
B : Prop
C : Prop
D : Prop
H : (A->B)/\(C->D)/\A/\C
====
B/\D
example < destruct H as [H1 [H2 [H3 H4]]].
1 subgoal

A : Prop
B : Prop
C : Prop
D : Prop
H1 : (A->B)
H2 : (C->D)
H3 : A
H4 : C
====
B/\D
example <
Now what? I simply want to prove that having A and A->B as hypothesis gives us B.

Then I use
split.
apply H1; assumption.
apply H2; assumption.
Qed.

Thanks for reading, but I solved my problems while writing this post. I realized that I had to destruct H as [H1 [H2 [H3 H4]]] and not as [H1 H2 H3 H4], as I originally tried to do (gave me errors ofc).