proposition: Lemma eta_expand Γ t A : neutral t → Γ |-- t => A -> Γ |-- η A t <= A.
proof: Proof. revert Γ t; induction A; intros; simp η; constructor; term. assert(0 < length (A1 :: Γ)) by (simpl; lia). specialize (IHA1 (A1 :: Γ) 0 (neutral_var _) (axiom_synth (A1 :: Γ) 0 H1)). apply (IHA2 (A1 :: Γ) @(lift 0 1 t, η A1 0)); term. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid