Sole using coq:

$1$ Implication

Prove that

$$ABCD in Prop,$($A $=$ B$)=($A $=$ C$)=($B $=$ C $=$ D$)=$ A $=$ D$.$ for which the Coq statement is

Lemma prob$1$ : forall A B C D : Prop, $($A $->$ B$)->($A $->$ C$)->($B $->$ C $->$ D$)->$ A $->$ D$.$

Use the template:

Require Import Arith.

Lemma prob$1$ : forall A B C D : Prop, $($A $->$ B$)->($A $->$ C$)->($B $->$ C $->$ D$)->$ A $->$ D$.$

Proof.

Qed.