proposition: Lemma equates_6 : forall y1 (P:A0->forall(x1:A1)(x2:A2 x1)(x3:A3 x2)(x4:A4 x3)(x5:A5 x4),Prop) x1 x2 x3 x4 x5 x6, P y1 x2 x3 x4 x5 x6 -> x1 = y1 -> P x1 x2 x3 x4 x5 x6.
proof: Proof. Proof using. intros. subst. auto. Qed.
imports: Coq.Lists.List