https://www.iij-ii.co.jp/activities/programming-coq/coqt1.html
これの練習問題の2つ目が分からない。
＞問1. 任意の命題 A B C に対して、「A ならば B ならば C」ならば「B ならば A ならば C」が成り立つ。

要するにこれはB⇒Aが可能なら、前提条件からA⇒Cだと思ったけど。
どう書くの？全然分からん

Definition prop4 : forall (A B C : Prop), (A -> B -> C) -> (B -> A -> C):=
fun A B C a b c => ?.