Inference of propositional witnesses?
Propositions have unique witnesses in any context. Could we allow these to be unmentioned, and infer them when applying judgements and operations?
Note that this inference goes the opposite way of the dependency based inference, so the interplay between these two might be complicated.