Library MetaRocq.PCUIC.Typing.PCUICNamelessTyp
From Stdlib Require Import RelationClasses.
From MetaRocq.Utils Require Import utils.
From MetaRocq.Common Require Import config.
From MetaRocq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICInduction
PCUICLiftSubst PCUICEquality PCUICReduction PCUICTyping PCUICPosition PCUICUnivSubst
PCUICNamelessDef PCUICGuardCondition PCUICNamelessConv PCUICConversion
PCUICWellScopedCumulativity PCUICOnFreeVars PCUICOnFreeVarsConv PCUICConfluence PCUICClosedTyp PCUICClosed
PCUICSigmaCalculus .
From Equations.Prop Require Import DepElim.
From Stdlib Require Import ssreflect ssrbool.
Implicit Types cf : checker_flags.
From MetaRocq.Utils Require Import utils.
From MetaRocq.Common Require Import config.
From MetaRocq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICInduction
PCUICLiftSubst PCUICEquality PCUICReduction PCUICTyping PCUICPosition PCUICUnivSubst
PCUICNamelessDef PCUICGuardCondition PCUICNamelessConv PCUICConversion
PCUICWellScopedCumulativity PCUICOnFreeVars PCUICOnFreeVarsConv PCUICConfluence PCUICClosedTyp PCUICClosed
PCUICSigmaCalculus .
From Equations.Prop Require Import DepElim.
From Stdlib Require Import ssreflect ssrbool.
Implicit Types cf : checker_flags.
Typing does not rely on name annotations of binders.
We prove this by constructing a type-preserving translation to
terms where all binders are anonymous. An alternative would be to
be parametrically polymorphic everywhere on the binder name type.
This would allow to add implicit information too.
Local Set Keyed Unification.
Set Default Goal Selector "!".