Library CoqFFI.Interface

Generalizable All Variables.
Set Implicit Arguments.

Class Inject (i m : Type → Type) :=
  inject : ∀ {a : Type}, i a → m a.