It may be possible to remove some of typing rule constructors in Syntax.Typing by showing that they are derivable (i.e., provable using other rules). cong_lam' and cong_pair' are two candidates which may follow from η laws. Or not! I haven't tried.
(Removing postulated typing rules is good because it makes proofs by mutual induction smaller.)
Update from @SSSPigeon : it doesn't seem like they are immediately derivable. The corresponding rules are derivable here because η laws are phrased using eliminators (e.g. f x = g x → f = g). Our rules use expansion (e.g. f = (λ. f v₀)), so the same derivation doesn't work.
It may be possible to remove some of typing rule constructors in Syntax.Typing by showing that they are derivable (i.e., provable using other rules).
cong_lam'andcong_pair'are two candidates which may follow from η laws. Or not! I haven't tried.(Removing postulated typing rules is good because it makes proofs by mutual induction smaller.)
Update from @SSSPigeon : it doesn't seem like they are immediately derivable. The corresponding rules are derivable here because η laws are phrased using eliminators (e.g.
f x = g x → f = g). Our rules use expansion (e.g.f = (λ. f v₀)), so the same derivation doesn't work.