proposition: Lemma args_for_related_noind_ind {T args0 args1} : @args_for_related T args0 args1 <-> @args_for_related_ind T args0 args1.
proof: Proof. split; intro H. { revert dependent args1; induction args0; intros; simpl in *; pose proof (invert_args_for_ex args1) as H'; simpl in *; subst; [ | solve [ repeat (intro || constructor) ] ]. destruct H' as [? [? H']]; subst; simpl in *. inversion H; constructor; eauto. } { induction H; simpl; intuition. } Qed.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations