proposition: Lemma refineFun_trans {fDom : list Type} {fCod : Type} : forall (fDef fDef' fDef'' : funType fDom fCod), refineFun fDef fDef' -> refineFun fDef' fDef'' -> refineFun fDef fDef''.
proof: Proof. induction fDom; simpl; intros. - rewrite H; eauto. - eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Sets.Ensembles Coq.ZArith.ZArith Coq.Classes.Morphisms Coq.Classes.SetoidTactics Fiat.Computation Fiat.Computation.SetoidMorphisms Coq.Logic.FunctionalExtensionality