Remove redundant types: Δ-Type, Δ-Context Checkpoint: To quantify Δ-environments (and Δ-terms) to rule out dishonesty.
Remove redundant types: Δ-Type, Δ-Context
Checkpoint: To quantify Δ-environments (and Δ-terms) to rule out
dishonesty.

Old-commit-hash: 787d5ee34634499c66203e78775cf7a3070dab95

inc-lc/ilc-agda