fact: Fixpoint aIn2 {M N : TypeCode -> Type} {A T} (v1 : M A) (v2 : N A) (args1 : args_for M T) : args_for N T -> Type := match args1 in args_for _ T return args_for _ T -> Type with | an_arg A' B' arg args => fun args2 => ({ pf : A' = A | eq_rect A' M arg A pf = v1 /\ eq_rect A' N (ahd args2) A pf = v2 } + @aIn2 _ _ _ _ v1 v2 args (atl args2))%type | noargs T => fun _ => False end.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations