let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
let module S = CicSubstitution in
let module C = Cic in
let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
let module S = CicSubstitution in
let module C = Cic in