fsdoc: no-summary-found
fsdoc: no-comment-found
* MAIN AXIOM ***
* DUPLICATED FOR GHOST FUNCTIONS
**val extensionality_g:a:Type -> b:Unidentified product: [a] Type -> f:arrow_g a b -> g:arrow_g a b -> (Lemma ((ensures (<==>(feq_g #a #b f g, ==(on_domain_g a f, on_domain_g a g))))) (Prims.Cons (SMTPat (feq_g #a #b f g)) (Prims.Nil )))Main axiom for ghost functions *