+ | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
+ let subst,metasenv,beta_expanded,ugraph1 =
+ beta_expand_many
+ test_equality_only metasenv subst context t2 args ugraph
+ in
+ fo_unif_subst test_equality_only subst context metasenv
+ (C.Meta (i,l)) beta_expanded ugraph1
+ | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
+ let subst,metasenv,beta_expanded,ugraph1 =
+ beta_expand_many
+ test_equality_only metasenv subst context t1 args ugraph
+ in
+ fo_unif_subst test_equality_only subst context metasenv
+ beta_expanded (C.Meta (i,l)) ugraph1