fact: Fixpoint decompose_lam_assum (Γ : context) (t : term) : context * term := match t with | tLambda n A B => decompose_lam_assum (Γ ,, vass n A) B | tLetIn na b bty b' => decompose_prod_assum (Γ ,, vdef na b bty) b' | _ => (Γ, t) end.
imports: MetaCoq.Template(All) MetaCoq.Utils(bytestring) List