proposition: Lemma args_eq_6 : forall (f:A1->A2->A3->A4->A5->A6->B) x1 y1 x2 y2 x3 y3 x4 y4 x5 y5 x6 y6, x1 = y1 -> x2 = y2 -> x3 = y3 -> x4 = y4 -> x5 = y5 -> x6 = y6 -> f x1 x2 x3 x4 x5 x6 = f y1 y2 y3 y4 y5 y6.
proof: Proof. Proof using. intros. subst. auto. Qed.
imports: Coq.Lists.List Coq.Logic.ProofIrrelevance