proposition: Lemma args_for_related_impl {M N P R T} args0 args1 : (P -> @args_for_related M N R T args0 args1) <-> @args_for_related M N (fun _ m n => P -> R _ m n) T args0 args1.
proof: Proof. revert dependent args1; induction args0; simpl in *; intros; pose proof (invert_args_for_ex args1) as H'; simpl in H'; subst; [ destruct H' as [? [? ?]]; subst | tauto ]; simpl in *. setoid_rewrite <- IHargs0. tauto. Qed.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations